This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE?03)
How to Compute the Refinement Relation for Parameterized Systems
Mont Saint-Michel, France
June 24-June 26
ISBN: 0-7695-1923-7
ASCII Text
x 
 
Francoise Bellegarde, Celina Charlet, Olga Kouchnarenko, "How to Compute the Refinement Relation for Parameterized Systems," Formal Methods and Models for Co-Design, ACM/IEEE International Conference on, pp. 103, First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE?03), 2003.
 
 
BibTex
x
 
@article{ 10.1109/MEMCOD.2003.1210095,
author = {Francoise Bellegarde and Celina Charlet and Olga Kouchnarenko},
title = {How to Compute the Refinement Relation for Parameterized Systems},
journal ={Formal Methods and Models for Co-Design, ACM/IEEE International Conference on},
volume = {0},
year = {2003},
isbn = {0-7695-1923-7},
pages = {103},
doi = {http://doi.ieeecomputersociety.org/10.1109/MEMCOD.2003.1210095},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Formal Methods and Models for Co-Design, ACM/IEEE International Conference on
TI - How to Compute the Refinement Relation for Parameterized Systems
SN - 0-7695-1923-7
SP
EP
A1 - Francoise Bellegarde,
A1 - Celina Charlet,
A1 - Olga Kouchnarenko,
PY - 2003
KW - null
VL - 0
JA - Formal Methods and Models for Co-Design, ACM/IEEE International Conference on
ER -
 
Francoise Bellegarde, Univ. Franche-Comte
Celina Charlet, Univ. Franche-Comte
Olga Kouchnarenko, Univ. Franche-Comte
In this paper 1, 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.
Citation:
Francoise Bellegarde, Celina Charlet, Olga Kouchnarenko, "How to Compute the Refinement Relation for Parameterized Systems," memocode, pp.103, First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE?03), 2003
Usage of this product signifies your acceptance of the Terms of Use.