Applied result detail

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

SMRČKA, A.; SEČKAŘOVÁ, P.

Original Title

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

English Title

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

Type

Software

Abstract

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.

Abstract in English

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.

Keywords

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

Key words in English

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

Location

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

Licence fee

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

www

https://www.fit.vut.cz/research/product/657/