Skip to Main content Skip to Navigation
Conference papers

Carmen: Software Component Model Checker

Ales Plsek 1, 2 Jiri Adamek 3 
1 JACQUARD - Weaving of Software Components
LIFL - Laboratoire d'Informatique Fondamentale de Lille, Inria Lille - Nord Europe
2 ADAM - Adaptive Distributed Applications and Middleware
LIFL - Laboratoire d'Informatique Fondamentale de Lille, Inria Lille - Nord Europe
Abstract : The challenge of model checking of isolated software components becomes more and more relevant with the boom of component-oriented technologies [20]. An important issue here is how to verify an open model representing an isolated software component (also referred as the missing environment problem in [17]). In this paper, we propose on-the-fly simulation of the component environment to address the issue. We employ behavior protocols [18] and a system coordinating two model checkers: Java PathFinder [4] and BPChecker [15]. This approach allows us to enclose the model represent- ing the behavior of a given component and consequently to exhaustively verify the model. Our solution was implemented as the Carmen tool [1]. We demonstrate scalability of our approach on real-life examples and show that, in comparison with the COMBAT model checker [17], we bring better performance, and also exhaustive and correct verification.
Document type :
Conference papers
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download
Contributor : Lionel Seinturier Connect in order to contact the contributor
Submitted on : Tuesday, May 27, 2008 - 2:23:53 PM
Last modification on : Friday, February 4, 2022 - 3:09:06 AM
Long-term archiving on: : Friday, May 28, 2010 - 6:07:04 PM


Files produced by the author(s)


  • HAL Id : inria-00282373, version 1



Ales Plsek, Jiri Adamek. Carmen: Software Component Model Checker. 4th International Conference on the Quality of Software Architecture (QoSA'08), Oct 2008, Karlsruhe, Germany. pp.71-85. ⟨inria-00282373⟩



Record views


Files downloads