Název: Bounded model checking v nástroji Java PathFinder
Překlad názvu: Bounded Model Checking Using Java PathFinder
Autoři: Dudka, Vendula ; Češka, Milan (oponent) ; Křena, Bohuslav (vedoucí práce)
Typ dokumentu: Diplomové práce
Rok: 2008
Jazyk: cze
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [cze] [eng]
Diplomová práce je věnovaná aplikaci formální metody bounded model checking pro automatickou opravu chyb. Oprava se specializuje na chyby spojené se souběžností. Práce je zaměřena na programy napsané v jazyce Java, a proto pro verifikační metodu byl zvolen model checker Java Pathfinder, který je určen pro Java programy. Vlastní verifikační metoda spočívá v aplikaci strategie pro navigaci stavovým prostorem do místa verifikace. Z daného místa je spuštěn bounded model checking pro ověření opravy. Navigace stavovým prostorem je implementována pomocí strategie record&replay trace. Pro aplikaci bounded model checkingu jsou implementovány další parametry a moduly pro verifikaci speciálních vlastností systému, které ověřují koreknost opravy chyby. Bounded model checking se provádí v okolí opravy. This thesis deals with the application of bounded model checking method for self-healing assurance of concurrency related problems. The self-healing is currently interested in the Java programming language. Therefore, it concetrate mainly on the model checker Java PathFinder which is built for handling Java programs. The verification method is implemented like the Record&Replay trace strategy for navigation through a state space and performance bounded model checking from reached state through the use of Record&Replay trace strategy. Java PathFinder was extended by new moduls and interfaces in order to perform the bounded model checking for self-healing assurance. Bounded model checking is applied at the neighbourhood of self-healing.
Klíčová slova: automatická oprava; Bounded model checking; Java PathFinder; Model Checking; ověřování opravy; Record&Replay trace; souběžnost; verifikace; Bounded model checking; concurrency; healing assurance; Java PathFinder; Model Checking; Record&Replay trace; self-healing; verification

Instituce: Vysoké učení technické v Brně (web)
Informace o dostupnosti dokumentu: Plný text je dostupný v Digitální knihovně VUT.
Původní záznam: http://hdl.handle.net/11012/53155

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-583152


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Vysoké učení technické v Brně
Vysokoškolské kvalifikační práce > Diplomové práce