How to Verify and Exploit a Refinement of Component-based Systems - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2006

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

Résumé

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.

Domaines

Autre [cs.OH]
Fichier principal
Vignette du fichier
RR-5898.pdf (335.13 Ko) Télécharger le fichier

Dates et versions

inria-00071369 , version 1 (23-05-2006)

Identifiants

  • HAL Id : inria-00071369 , version 1

Citer

Olga Kouchnarenko, Arnaud Lanoix. How to Verify and Exploit a Refinement of Component-based Systems. [Research Report] RR-5898, INRIA. 2006. ⟨inria-00071369⟩
144 Consultations
145 Téléchargements

Partager

Gmail Facebook X LinkedIn More