Carmen: Software Component Model Checker

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F08%3A00317133" target="_blank" >RIV/67985807:_____/08:00317133 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Carmen: Software Component Model Checker

Original language description

The challenge of model checking of isolated software components becomes more and more relevant with the boom of component-oriented technologies. An important issue here is how to verify an open model representing an isolated software component (also referred as the missing environment problem in). In this paper, we propose on-the-fly simulation of the component environment to address the issue. We employ behavior protocols and a system coordinating two model checkers: Java PathFinder and BPChecker. Thisapproach allows us to enclose the model representing the behavior of a given component and consequently to exhaustively verify the model. Our solution was implemented as the Carmen tool. We demonstrate scalability of our approach on real-life examples and show that, in comparison with the COMBAT model checker, we bring better performance, and also exhaustive and correct verification.

Czech name

Carmen: Model checker softwarových komponent

Czech description

Verifikace chování izolovaných softwarových komponent představuje problém, jehož význam roste s nástupem technologií orientovaných na komponenty a jejich skládání jako způsob tvorby složitých softwarových systémů. Specifickým problémem je verifikace otevřeného modelu chování izolované komponenty, tj. Komponenty, která není součástí žádné aplikace. V článku navrhujeme řešení tohoto problému pomocí simulace chybějícího prostředí během verifikace. K popisu chování používáme protokoly chování (tzv. behaviorprotocols) a systém, který umožňuje koordinovat dva model checkery: Java PathFinder a BPChecker. Tento postup nám umožňuje zapouzdřit model reprezentující chování komponenty a jeho následnou verifikaci. Řešení bylo implementováno v softwarovém nástrojiCarmen. V článku rovněž ukazujeme škálovatelnost našeho řešení na reálných problémech, přičemž ve srovnání s model checkerem COMBAT dosahujeme vyššího výkonu a verifikaci celého stavového prostoru chování komponenty.

Type

D - Article in proceedings

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

—

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2008

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

Quality of Software Architectures. Models and Architectures

ISBN

978-3-540-87878-0

ISSN

—

e-ISSN

—

Number of pages

15

Pages from-to

—

Publisher name

Springer

Place of publication

Berlin

Event location

Karlsruhe

Event date

Oct 14, 2008

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000260962900005