ACCUEIL

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

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 25/1 - 2006  - pp.73-102  - doi:10.3166/tsi.25.73-102
TITRE
Propriétés dynamiques avec hypothèses d'équité en B événementiel

RÉSUMÉ
Nous présentons une approche à la spécification, preuve et raffinement de propriétés de vivacité sous hypothèse d'équité faible dans le B événementiel. Les propriétés de vivacité sont divisées en deux classes : propriétés de base et propriétés générales. Nous donnons des obligations de preuve fondées sur le calcul des plus faibles préconditions pour prouver les propriétés de base. Les propriétés de vivacité générales sont prouvées par les définitions et théorèmes de la logique U N I T Y. Nous donnons les obligations de preuve de la préservation des propriétés de vivacité dans le raffinement. Notre démarche est illustrée par un exemple d'un système de gestion de processus.


ABSTRACT
We present an approach to specification, proof and refinement of liveness properties under weak fairness assumptions in B event systems. Liveness properties are divided in two classes: basic properties and general properties. We give proof obligations by calculus of weakest preconditions in order to prove basic properties. General liveness properties are proved by definitions and theorems of the logic programming of U N I T Y. We give proof obligations of the preservation of liveness properties in the refinement. Our approach is showed by an example of a system modeling management of processes.


AUTEUR(S)
Héctor Ruíz BARRADAS, Didier BERT

MOTS-CLÉS
B événementiel, UNITY, propriétés de vivacité, équité faible.

KEYWORDS
event B, UNITY, liveness properties, weak fairness.

LANGUE DE L'ARTICLE
Français

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



Mot de passe oublié ?

ABONNEZ-VOUS !

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

 English version >> 
Lavoisier