Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution

Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

SLABÝ Jiří STREJČEK Jan TRTÍK Marek

Rok publikování 2012
Druh Článek ve sborníku
Konference Formal Methods for Industrial Critical systems: 17th International Workshop, FMICS 2012
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www http://www.springerlink.com/content/p027081716330416/
Doi http://dx.doi.org/10.1007/978-3-642-32469-7_14
Obor Informatika
Klíčová slova Bug finding; Symbolic execution; Program slicing; FSM property specification; Code instrumentation
Přiložené soubory
Popis Představujeme novou techniku pro ověřování vlastností popsaných konečně-stavovými stroji. Tato technika je založena na synergii tří známých metod: instrumentace, prořezání programu a symbolické vykonání. Přesněji, instrumentujeme daný program kódem, který sleduje běh stavových strojů představujících různé vlastnosti. Dále program prořežeme, abychom zmenšili jeho velikost při zachování běhů stavových strojů. Nakonec prořezaný program symbolicky vykonáme, abychom našli skutečné porušení ověřovaných vlastností, t.j. skutečné chyby. Podle použitého druhu symbolického vykonání může být tato technika použita jako samostatná metoda pro detekci chyb nebo k vytřídění některých falešných hlášení z výstupu jiných nástrojů pro detekci chyb. Poskytujeme několik příkladů, které dokumentují praktickou použitelnost naší techniky.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.