How to compute the refinement relation for parameterized systems

Author

Bellegarde, Françoise ; Charlet, Célina ; Kouchnarenko, Olga

Author_Institution

LIFC, Univ. Franche-Comte, Besancon, France

fYear

2003

Firstpage

103

Lastpage

112

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 (Abdulla et al., 199) 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 of the property (safety and PLTL properties) preservation by refinement for their verification.

Keywords

formal verification; refinement calculus; systems analysis; PLTL property; computer system; infinite state machine; model checking; parameterized system; proof technique; refinement relation; refinement verification; regular language; safety property; state representation; symbolic model; system analysis; transducer transition; Acceleration; Application software; Concrete; Counting circuits; Data structures; Humans; Logic; Reachability analysis; Safety; Transducers;

fLanguage

English

Publisher

ieee

Conference_Titel

Formal Methods and Models for Co-Design, 2003. MEMOCODE '03. Proceedings. First ACM and IEEE International Conference on

Conference_Location

Mont Saint Michel, France

Print_ISBN

0-7695-1923-7

Type

conf

DOI

10.1109/MEMCOD.2003.1210095

Filename

1210095