MOVEC is an automated tool for runtime MOnitoring, VErification and Control of C programs as an extension to the C programming language. MOVEC provides a source-to-source transformation that automatically weaves monitor specifications written in MOVEC into MOVEC-unaware C programs, and generates instrumented C programs which can be compiled by any compliant C compiler such as GCC and other platform-specific compilers. In other words, MOVEC integrates and extends aspect-oriented programming (AOP) and monitoring-oriented programming (MOP), and is an implementation of these ideas for the C programming language.
To run it, please unzip the gzip file, and put its directory to your PATH. Note that:
- MOVEC is developed and tested under Ubuntu Linux 64-bit. It may also work under other Linux releases, but we cannot guarantee that.
- You can use "movec --version" to show its version, "movec -h" to show user instructions. But note that some of the listed options are not available in this version, and using them takes no effect.
- If you are not familiar with the syntax and user instructions, please learn from the examples and benchmarks.
The MOVEC Reference Manual (TBA) gives a tutorial from a user's point of view and describes how to write monitor specifications and run the tool.
Zhe Chen, Zhemin Wang, Yunlong Zhu, Hongwei Xi, Zhibin Yang.
Parametric Runtime Verification of C Programs.
In Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), Eindhoven, The Netherlands, Lecture Notes in Computer Science, vol. 9636, pp. 299-315. Springer, 2016.