Testos-Spectra is a verification tool implementing run-time verification of past-time LTL (ptLTL) formulae. It is based on translation of ptLTL formula to a run-time monitor which is instrumented to a C/C++ programs. If a program run invalidates the formula, the monitor will report it as failed assertion.
Currently, installation is available for Linux and Mac OS. Extract, and compile the tool using make. Perform unit tests using make test.
$ tar xzf spectra-0.5.tgz $ cd spectra-0.5 $ make $ make test
Using Spectra for your own project, you will need:
Build your monitor from the specification using spectra, then compile and run your SUT:
$ ./spectra --tpc -s ptltl.spec -d sut.h
Formulae from specification will be translated and compiled into a static library libspectra.a. A new header file monitor.h containing definitions of monitoring functions will be created and the source code of SUT (referenced by specification file, cf. T-Props_Checker/InputFileSpec.md for more details) will be updated = instrumented with monitor invocations.
$ cc -c sut.c $ cc -L. sut.o -lspectra -o sut $ ./sut
For more information, contact Ales Smrcka.
The code in this project is licensed under BSD-3-Clause.
This project has received funding from the Technology Agency of the Czech Republic (TACR) under the project Aufover TH04010192.