Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution
| Autoři | |
|---|---|
| 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 | |
| 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: |