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

Název česky

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

Typ

software

Licence

K využití výsledku jiným subjektem je vždy nutné nabytí licence

Licenční poplatek

Poskytovatel licence na výsledek nepožaduje licenční poplatek

Autoři

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

Klíčová slova

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

Popis

Nástroj slouží pro verifikaci vlastností za běhu programu. Testování programů je založeno na překladu vlastností v logice ptLTL do monitorů běhu programu, které jsou instrumentovány do zdrojových souborů testovaného systému. Jakmile monitor odhalí porušení nějaké vlastnosti, informuje uživatele o tom, ve kterém případu porušení nastalo a proč je která vlastnost porušena.

Umístění

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

Licenční podmínky

Licenční podmínky v souladu s licení BSD-3-Clause dostupné na https://opensource.org/licenses/BSD-3-Clause

Projekty

Verifikace a validace spolehlivosti a bezpečnosti automatizovaných systémů, MŠMT, Společná technologická iniciativa ECSEL, 8A20009, 2020-2023, řešení

Výzkumné skupiny

Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)

Pracoviště

Ústav inteligentních systémů (UITS)