Testos-Spectra: A tool for verification of ptLTL on C/C++ programs

Czech title

Testos-Spectra: Nástroj pro verifikaci ptLTL na programech C/C++

Type

software

License

In order to use the result by another entity, it is always necessary to acquire a license

License Fee

The licensor does not require a license fee for the result

Authors

Smrčka Aleš, Ing., Ph.D. (DITS)
Sečkařová Petra, Ing.

Keywords

Testing, Run-time verification, LTL verification, Source code verification

Description

The tool is for verification of safety properties during the run-time. The testing is based on translation of ptLTL formulae into a run-time monitor which are instrumented into source codes of system under test (SUT). Once the monitor witnesses a violation of the specification, it reports when such a case occurs providing data why the given formula has been violated.

Location

Domovská stránka nástroje včetně samotného nástroje je: http://www.fit.vutbr.cz/research/groups/verifit/tools/testos-spectra/

License Conditions

Licence BSD-3-Clause available here: https://opensource.org/licenses/BSD-3-Clause

Projects

Verification and Validation of Automated Systems' Safety and Security, MŠMT, Společná technologická iniciativa ECSEL, 8A20009, 2020-2023, running

Research groups

Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)

Departments

Department of Intelligent Systems (DITS)