Model checking softwarových komponent: kombinace Java PathFinder a Behavior Protocol model checker

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

—

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.

Druh

D - Stať ve sborníku

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

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)

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ů

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

—