Using Acceleration to Compute Parameterized System Refinement - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2003

Using Acceleration to Compute Parameterized System Refinement

Résumé

In this paper, we present a verification approach for a class of parameterized systems. These systems are composed of an arbitrary number of similar processes. As in \cite{abdulla99b} we represent the states by regular languages and the transitions by transducers over regular languages. If we can compute a symbolic model by acceleration of the actions, then we can also verify a refinement relation R between the symbolic models. We show that, under some conditions, if R is verified between two symbolic models, then refinement is verified between concrete parameterized systems. Then, we can take advantage the property (safety and PLTL properties) preservation by refinement for their verification.

Domaines

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

Dates et versions

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

Identifiants

  • HAL Id : inria-00071870 , version 1

Citer

Françoise Bellegarde, Célina Charlet, Olga Kouchnarenko. Using Acceleration to Compute Parameterized System Refinement. [Research Report] RR-4716, INRIA. 2003, pp.18. ⟨inria-00071870⟩
69 Consultations
66 Téléchargements

Partager

Gmail Facebook X LinkedIn More