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 44/9-10 - 2010  - pp.1119-1163  - doi:10.3166/jesa.44.1119-1163
TITRE
B événementiel et les propriété de vivacité

TITLE
Event-B method and liveness properties

RÉSUMÉ
Dans cet article, nous nous intéressons à la vérification de propriétés de vivacité sur des systèmes réactifs. Nous nous basons sur B événementiel pour la spécification et la validation de tels systèmes. En considérant la limitation de B aux propriétés d’invariance, nous proposons d’appliquer le langage TLA+ pour la vérification des propriétés de vivacité. Nous étendons, en particulier, l’expressivité et la sémantique d’un modèle B pour obtenir un modèle B temporel. En transformant le modèle B étendu en un module TLA+ grâce à un prototype (B2TLA+) que nous avons développé, nous pouvons vérifier ces propriétés sur des systèmes à états finis grâce au model-checker TLC. Pour la vérification de ces types de propriétés sur des systèmes à états infinis, nous utilisons les diagrammes de prédicats.


ABSTRACT
This paper deals with the verification of liveness properties on reactive systems. We are based on the event B method to specify and validate such systems. By considering the limitation of the B to invariance properties, we propose to apply the language TLA+ to verify liveness properties on a software behavior. We extend, in particular, the expressivity and the semantics of the event B method to deal with the specification n of fairness and eventuality properties. By transforming an extended B model into TLA+ module by using a prototype system (B2TLA+) that we have developed, we can verify these properties thanks to the modelchecker TLC on finite state systems. For the verification of infinite-state systems, we propose the use of predicate diagrams.


AUTEUR(S)
Olfa MOSBAHI, Jacques JARAY

MOTS-CLÉS
spécification, propriété d’�quité, propriété de fatalité, raffinement, vérification.

KEYWORDS
specification, fairness properties, eventuality properties, refinement, verification.

LANGUE DE L'ARTICLE
Anglais

 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  (791 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

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

 English version >> 
Lavoisier