|
|
Ověřování asercí kódu pomocí zpětné symbolické exekuce
Husák, Robert ; Kofroň, Jan (vedoucí práce) ; Parízek, Pavel (oponent)
Pro prevenci, odhalování a opravování chyb v softwaru existuje celá řada nástrojů pro programátory, přičemž některé z nich umožňují pracovat přímo se sémantikou programu. V případě jazyka C# jsou hlavními zástupci Microsoft FxCop, Code Contracts a Pex. Použití těchto nástrojů může velkou měrou přispět k vysoké spolehlivosti programů. Jejich úplné zapojení do procesu vývoje software ve firmách je bohužel značně náročné na prostředky. Z tohoto důvodu jsme vytvořili AskTheCode, zjednodušený nástroj pro verifikaci asercí kódu. Jeho hlavním účelem je pomoci uživateli s jedním konkrétním problémem, který v daném okamžiku řeší. Vzhledem k tomuto přístupu jsme jej implementovali pomocí zpětné symbolické exekuce. Přestože je momentálně schopen pracovat pouze se základními konstrukty a typy jazyka C#, srovnání s existujícími nástroji ukázalo, že při dalším rozvoji má potenciál poskytnout uživateli významnou přidanou hodnotu. Powered by TCPDF (www.tcpdf.org)
|
|
| |
|
| |
|
| |
|
|
Heuristická redukce paralelismu v prostředí komponenty
Pařízek, P. ; Plášil, František
Při model checkingu kódu softwarových komponent, které se vyznačují vysokou úrovní paralelismu, se často vyskytne problem exploze stavového prostoru, bez ohledu na to, že jedna komponenta má obvykle menší stavový prostor než celý systém. Zde prezentujeme techniku, která adresuje problém exploze stavového prostoru pro ověřování kódu primitivních komponent s Java PathFinder v případě, že ověřovaná vlastnost je absence synchronizačních chyb. Klíčová myšlenka je redukce paralelismu v prostředí komponenty tak, že pouze ty části kódu komponenty, které pravděpodobně mohou vyvolat synchronizační chybu, jsou vykonány paralelně; takové části jsou identifikovány pomocí heuristické statické analýzy kódu (hledáním podezřelých vzorů v kódu komponenty). Výhody této techniky, t.j. podpora objevení synchronizačních chyb v omezeném čase a prostoru a reportování čitelnějších protipříkladů, jsou ilustrovány na výsledcích několika experimentů.
|
|
|
Model checking softwarových komponent: úprava Java PathFinder pro spolupráci s Behavior Protocol Checker
Pařízek, P. ; Plášil, František ; Kofroň, Jan
Přestože existuje několik model checkerů pro software, které ověřují kód proti specifikaci zapsané např. v temporální logice a tzv. assertions, nebo ověřují nízkoúrovňové vlastnosti (jako neošetřené výjimky), žádný z nich nepodporuje ověřování softwarových komponent proti vyšší specifikaci chování. Tato zpráva popisuje náš přístup k model checkingu softwarových komponent implementovaných v jazyce Java proti specifikaci jejich chování definované pomocí protokolů chování, který využívá model checker Java PathFinder a protocol checker. Vlastnosti ověřované nástrojem Java PathFinder (korektnost sekvencí volání metod) se validují pomocí spolupráci s nástrojem protocol checker. Ukazujeme, že pouze návrhový vzor publisher/listener, označovaný za klíčový pro podporu rozšiřitelnosti v nástroji Java PathFinder, nebyl dostatečný pro tento typ ověřování (přestože byl pro nás velmi užitečný).
|
|
| |
|
| |
|
| |
|
| |
host ::
RSS.