Přehled o publikaci
2012
Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution
SLABÝ, Jiří; Jan STREJČEK and Marek TRTÍKBasic information
Original name
Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution
Authors
SLABÝ, Jiří; Jan STREJČEK and Marek TRTÍK
Edition
Berlin, Heidelberg, Formal Methods for Industrial Critical systems: 17th International Workshop, FMICS 2012, p. 207-221, 15 pp. 2012
Publisher
Springer
Other information
Language
English
Type of outcome
Proceedings paper
Field of Study
Informatics
Country of publisher
Germany
Confidentiality degree
is not subject to a state or trade secret
Publication form
printed version "print"
References:
Marked to be transferred to RIV
Yes
RIV identification code
RIV/00216224:14330/12:00057431
Organization
Fakulta informatiky – Repository – Repository
ISBN
978-3-642-32468-0
ISSN
Keywords in English
Bug finding; Symbolic execution; Program slicing; FSM property specification; Code instrumentation
Links
GBP202/12/G061, research and development project. MUNI/A/0914/2009, interní kód Repo.
Changed: 1/9/2020 12:27, RNDr. Daniel Jakubík
In the original language
We introduce a novel technique for checking properties described by finite state machines. The technique is based on a synergy of three well-known methods: instrumentation, program slicing, and symbolic execution. More precisely, we instrument a given program with a code that tracks runs of state machines representing various properties. Next we slice the program to reduce its size without affecting runs of state machines. And then we symbolically execute the sliced program to find real violations of the checked properties, i.e. real bugs. Depending on the kind of symbolic execution, the technique can be applied as a stand-alone bug finding technique, or to weed out some false positives from an output of another bug-finding tool. We provide several examples demonstrating the practical applicability of our technique.
In Czech
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.
