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.

Model based testing
Runtime verification and online testing
Monitoring and logs analysis
Full coverage test generation
LTL monitoring
Regular expressions monitoring
main contact: 
Viorel Preoteasa


LIME Testbench sofware can be downloaded from the link below. The zip file contains a file REDME.txt with instructions about compiling and testing all components


Instructions about compiling and testing all Lime Testbench components are placed in the REDME.txt included within the downloadable Lime Testbench zip file (see link above). More detailed documentation is available in the folder LimeTB/doc.

Source Code

LIME Testbench source code can be downloaded from the link below