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

Základní údaje

Originální název Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution
Autoři

Další údaje

Citace SLABÝ, Jiří, Jan STREJČEK a Marek TRTÍK. Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution. In Mariëlle Stoelinga, Ralf Pinger. Formal Methods for Industrial Critical systems: 17th International Workshop, FMICS 2012. Berlin, Heidelberg: Springer, 2012. s. 207-221, 15 s. ISBN 978-3-642-32468-0. doi:10.1007/978-3-642-32469-7_14.
Originální název angličtina
Obor Informatika
WWW
Druh Článek ve sborníku
Klíčová slova Bug finding; Symbolic execution; Program slicing; FSM property specification; Code instrumentation

Anotace

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.

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

Další info