ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne

APPEL À
CONTRIBUTION

Le comité de rédaction du JESA lance un appel à proposition de numéros spéciaux.

En savoir plus >>
Autres revues >>

Journal Européen des Systèmes Automatisés

1269-6935
Revues des Systèmes
 

 ARTICLE VOL 39/1-3 - 2005  - pp.239-254  - doi:10.3166/jesa.39.239-254
TITRE
Vérification de systèmes hiérarchiques par raffinement

RÉSUMÉ
Cet article traite de la spécification et de la vérification par model-checking des systèmes hiérarchiques réactifs. Le modèle utilisé est celui des automates hiérarchiques dans lesquels nous exploitons la décomposition d'un état en un ensemble d'automates acycliques. Pour pallier au problème de l'explosion combinatoire en nombre d'états induit par le modelchecking, nous proposons d'utiliser la technique du raffinement. La contribution de ce papier est de définir les conditions de raffinement entre automates hiérarchiques de telle sorte que leurs modèles qui sont des structures de Kripke se raffinent. Cette propriété permet de préserver les propriétés de logique temporelle linéaire sur les structures de Kripke. La vérification des propriétés ne s'effectuent que sur le modèle abstrait de plus petite taille.


ABSTRACT
This article treats the specification and verification by model-checking the reactive hierarchical systems. The model used is the hierarchical automata which exploits the decomposition of a state in to a set of acyclic automata. In order to deal with the problem of the state explosion induced by the model-checking, we propose to use the technique of refinement. The contribution of this paper is to define the conditions of refinement between hierarchical automata. This refinement involves the refinement of their models which are Kripke structures. This property is necessary to preserve the properties of linear temporal logic on the Kripke structures. The properties are verified only on the abstract model with small size.


AUTEUR(S)
Mohammed AL ACHHAB, Ahmed HAMMAD, Hassan MOUNTASSIR

MOTS-CLÉS
spécification, vérification, raffinement, automate hiérarchique, structure de Kripke.

KEYWORDS
specification, verification, rafinement, hierarchical automata, Kripke structure.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 7.5 €
• Non abonné : 15.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (244 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier