Raffiner pour vérifier des systèmes paramétrés
Nous présentons la vérification des systèmes paramétrés pour lesquels le paramètre
est un nombre arbitraire de processus similaires. Nous utilisons une représentation empruntée
à [ABD 99b] des états et des transitions du modèle respectivement par des langages réguliers
et des transducteurs entre langages réguliers. Quand nous savons calculer un modèle symbolique
abstrait où les états sont des ensembles réguliers et les transitions sont des accélérations
des actions, nous pouvons vérifier le raffinement des systèmes ainsi que leurs propriétés. Ces
propriétés peuvent être des propriétés de sûreté et plus généralement des propriétés
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. Like [ABD 99b] we represent the states by regular languages and the transitions by transducers over regular languages. If we can calculate a symbolic model by acceleration of the actions, then we can verify refinement between systems and their properties. These properties are safety properties and, more generally, È ÄÌ Ä properties about the global behavior of the system. Our goal is to integrate these tehniques in a refinement based developpement. Then, we take advantage of the preservation of the properties by refinement for their verification.
F.BELLEGARDE, C.CHARLET, O.KOUCHNARENKO
systèmes paramétrés, vérification, propriétés, langages réguliers, raffinement.
Paramaterized systems, verification, properties, regular languages, refinement.
Français
|
