Carmen: Model checker softwarových komponent

Kód výsledku v 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>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Carmen: Software Component Model Checker

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Carmen: Software Component Model Checker

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

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

OECD FORD obor

—

Projekt

—

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2008

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

Quality of Software Architectures. Models and Architectures

ISBN

978-3-540-87878-0

ISSN

—

e-ISSN

—

Počet stran výsledku

15

Strana od-do

—

Název nakladatele

Springer

Místo vydání

Berlin

Místo konání akce

Karlsruhe

Datum konání akce

14. 10. 2008

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000260962900005