How to Verify and Exploit a Refinement of Component-based Systems

Olga Kouchnarenko 1 Arnaud Lanoix 2, 3
2 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
3 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In order to deal with the verification of large systems, compositional approaches postpone in part the problem of combinatorial explosion during model exploration. The purpose of the work we present in this paper is to establish a compositional framework in which the verification may proceed through a refinement-based specification and a component-based verification approaches. A constraint synchronised product operator enables us 1) an automated compositional verification of a component-based system refinement relation, and 2) safety LTL properties of a whole system from local safety LTL properties of its components. The main advantage of our specification and verification approaches is that LTL properties are preserved through composition and refinement.
Type de document :
Rapport
[Research Report] RR-5898, INRIA. 2006
Liste complète des métadonnées

https://hal.inria.fr/inria-00071369
Contributeur : Rapport de Recherche Inria <>
Soumis le : mardi 23 mai 2006 - 16:56:26
Dernière modification le : vendredi 6 juillet 2018 - 15:06:08
Document(s) archivé(s) le : dimanche 4 avril 2010 - 22:07:22

Fichiers

Identifiants

  • HAL Id : inria-00071369, version 1

Citation

Olga Kouchnarenko, Arnaud Lanoix. How to Verify and Exploit a Refinement of Component-based Systems. [Research Report] RR-5898, INRIA. 2006. 〈inria-00071369〉

Partager

Métriques

Consultations de la notice

252

Téléchargements de fichiers

229