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

https://hal.inria.fr/inria-00282373
Contributor : Lionel Seinturier <>
Submitted on : Tuesday, May 27, 2008 - 2:23:53 PM
Last modification on : Thursday, February 21, 2019 - 10:52:48 AM
Long-term archiving on: : Friday, May 28, 2010 - 6:07:04 PM

File

carmen-camera-modif.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00282373, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

362

Files downloads

396