Název: Model Checking of Software Components: Making Java PathFinder Cooperate with Behavior Protocol Checker
Překlad názvu: Model checking softwarových komponent: úprava Java PathFinder pro spolupráci s Behavior Protocol Checker
Autoři: Pařízek, P. ; Plášil, František ; Kofroň, Jan
Typ dokumentu: Výzkumné zprávy
Rok: 2006
Jazyk: eng
Edice: Technical Report, svazek: 2006/2
Abstrakt: [eng] [cze]
Although there exist several software model checkers that check the code against properties specified e.g. via a temporal logic and assertions, or just verifying low-level properties (like unhandled exceptions), none of them supports checking of software components against a high-level behavior specification. We present our approach to model checking of software components implemented in Java against a high-level specification of their behavior defined via behavior protocols 1 which employs the Java PathFinder model checker and the protocol checker. The property checked by the Java PathFinder (JPF) tool (correctness of particular method call sequences) is validated via its cooperation with the protocol checker. We show that just the publisher/listener pattern claimed to be the key flexibility support of JPF (even though proved very useful for our purpose) was not enough to achieve this kind of checking. 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ý).
Klíčová slova: behavior protocols; formal verification; Java PathFinder; software components
Číslo projektu: CEZ:AV0Z10300504 (CEP), GD201/05/H014 (CEP), 1ET400300504 (CEP)
Poskytovatel projektu: GA ČR, GA AV ČR

Instituce: Ústav informatiky AV ČR (web)
Informace o dostupnosti dokumentu: Dokument je dostupný v příslušném ústavu Akademie věd ČR.
Původní záznam: http://hdl.handle.net/11104/0148105

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


Záznam je zařazen do těchto sbírek:
Věda a výzkum > AV ČR > Ústav informatiky
Zprávy > Výzkumné zprávy