HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Using Acceleration to Compute Parameterized System Refinement

Françoise Bellegarde Célina Charlet 1 Olga Kouchnarenko 1
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : 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.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 7:03:51 PM
Last modification on : Friday, January 21, 2022 - 3:09:04 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:42:09 PM


  • HAL Id : inria-00071870, version 1


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⟩



Record views


Files downloads