Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker

Result code in 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>

Alternative codes found

RIV/00216208:11320/07:10084051

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker

Original language description

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.

Czech name

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

Czech description

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 JavaPathFinder 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ý).

Type

D - Article in proceedings

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

<a href="/en/project/GA201%2F06%2F0770" target="_blank" >GA201/06/0770: Formal methods applicable to development of component-based systems</a><br>

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2007

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Proceedings of 30th IEEE/NASA Software Engineering Workshop

ISBN

0-7695-2624-1

ISSN

—

e-ISSN

—

Number of pages

9

Pages from-to

133-141

Publisher name

IEEE Computer Society

Place of publication

Los Alamitos

Event location

Loyola College Graduate Center, Columbia

Event date

Apr 24, 2006

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—