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.
Type de document :
Communication dans un congrès
4th International Conference on the Quality of Software Architecture (QoSA'08), Oct 2008, Karlsruhe, Germany. pp.71-85, 2008
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00282373
Contributeur : Lionel Seinturier <>
Soumis le : mardi 27 mai 2008 - 14:23:53
Dernière modification le : jeudi 11 janvier 2018 - 06:22:13
Document(s) archivé(s) le : vendredi 28 mai 2010 - 18:07:04

Fichier

carmen-camera-modif.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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, 2008. 〈inria-00282373〉

Partager

Métriques

Consultations de la notice

274

Téléchargements de fichiers

128