Propriétés dynamiques avec hypothèses d'équité en B événementiel
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.
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.
H.BARRADAS, D.BERT
B événementiel, UNITY, propriétés de vivacité, équité faible.
event B, UNITY, liveness properties, weak fairness.
Français
|
