Model checking softwarových komponent: kombinace Java PathFinder a Behavior Protocol model checker
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F06%3A00090230" target="_blank" >RIV/67985807:_____/06:00090230 - isvavai.cz</a>
Nalezeny alternativní kódy
RIV/00216208:11320/07:10084051
Výsledek na webu
—
DOI - Digital Object Identifier
—
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker
Popis výsledku v původním jazyce
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 softwarecomponents 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/listenerpattern 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.
Název v anglickém jazyce
Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker
Popis výsledku anglicky
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 softwarecomponents 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/listenerpattern 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.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
JC - Počítačový hardware a software
OECD FORD obor
—
Návaznosti výsledku
Projekt
<a href="/cs/project/GA201%2F06%2F0770" target="_blank" >GA201/06/0770: Formální metody prakticky použitelné pro vývoj systémů složených ze softwarových komponent</a><br>
Návaznosti
Z - Vyzkumny zamer (s odkazem do CEZ)
Ostatní
Rok uplatnění
2007
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
Proceedings of 30th IEEE/NASA Software Engineering Workshop
ISBN
0-7695-2624-1
ISSN
—
e-ISSN
—
Počet stran výsledku
9
Strana od-do
133-141
Název nakladatele
IEEE Computer Society
Místo vydání
Los Alamitos
Místo konání akce
Loyola College Graduate Center, Columbia
Datum konání akce
24. 4. 2006
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—