LIME Testbench

The LIME Testbench (SSF) is a testing and runtime monitoring tool originally developed in the project LightweIght formal Methods for distributed component-based Embedded systems (LIME), and it's continuation project LIME2. The LIME Testbench implements two separate functions: runtime monitoring of model-based properties, and test case generation. Both functions rely on the instrumentation and monitoring of the execution of the program under test. Instrumenting the program under test allows to monitor and record all function calls, memory access, and register operations during execution without additional effort from the programmer. This in turn allows to add assertions to the program to monitor adherence to properties that can be specified with regular expressions, temporal logic, or finite state machines. It is also possible to automatically generate high coverage test suites by using a constraint solver to produce inputs that force the program to take certain branches during execution. The above features work for Java, but there is also a C version that supports the generation of test cases.

LIME TB is developed further in MegaM@art2 project, to make it compatible with the newest development tools, and to extend all its components for the C/C++ programming language.