How to Compute the Refinement Relation for Parameterized Systems

First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE’03) p. 103
How to Compute the Refinement Relation for Parameterized Systems
Francoise Bellegarde, Univ. Franche-Comte
Celina Charlet, Univ. Franche-Comte
Olga Kouchnarenko, Univ. Franche-Comte

Full Article Text:

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/MEMCOD.2003.1210095
Send link to a friend

Abstract
In this paper ¹, we present a refinement verification for a class of parameterized systems. These systems are composed of an arbitrary number of similar processes. As in [4] 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.
Back to Top Additional Information
Citation: Francoise Bellegarde, Celina Charlet, Olga Kouchnarenko, "How to Compute the Refinement Relation for Parameterized Systems," memocode, p. 103, First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE’03), 2003

	Advanced Search
CS Search Google Search