0317133 - ÚI 2009 RIV DE eng C - Conference Paper (international conference)
Plšek, A. - Adámek, Jiří
Carmen: Software Component Model Checker.
[Carmen: Model checker softwarových komponent.]
Quality of Software Architectures. Models and Architectures. Berlin: Springer, 2008 - (Becker, S.; Plášil, F.; Reussner, R.), s. 71-85. Lecture Notes in Computer Science, 5281. ISBN 978-3-540-87878-0.
[QoSA 2008. International Conference on the Quality of Software Architectures /4./. Karlsruhe (DE), 14.10.2008-17.10.2008]
Grant - others:GA ČR(CZ) GA201/08/0266; ANR/RNTL(FR) Flex-eWare; Belgian Science Policy(BE) Interuniversity Attraction Poles Programme
Institutional research plan: CEZ:AV0Z10300504
Keywords : software components * behavior specification * model-checking
Subject RIV: JC - Computer Hardware ; Software

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. This approach 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.

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. behavior protocols) 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ástroji Carmen. 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.
Permanent Link: http://hdl.handle.net/11104/0166859