Specification and Proof of Liveness Properties in B Event Systems

Olfa Mosbahi 1 Jacques Jaray 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In this paper, we give a framework for defining an extension to the event B method. The event B method allows us to state only invariance properties, but in some applications such as automated or distributed systems, fairness and eventuality properties must also be considered. We first extend the expressiveness of the event B method to deal with the specification of these properties. Then, we give a semantics of this extended syntax over traces, in the same spirit as the temporal logic of actions TLA does. Finally, we give verification rules of these properties. We denote by temporal B model, the B model extended with liveness properties. We illustrate our method on a case study related to automated system.
Type de document :
Communication dans un congrès
Joaquim Filipe and Boris Shishkov and Markus Helfert. 2nd International Conference on Software and Data Technologies - ICSOFT 2007, Jul 2007, Barcelone, Spain. INSTICC Press, pp.25-34, 2007
Liste complète des métadonnées

Littérature citée [10 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00158906
Contributeur : Olfa Mosbahi <>
Soumis le : lundi 2 juillet 2007 - 00:15:08
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52
Document(s) archivé(s) le : lundi 24 septembre 2012 - 10:46:54

Fichier

mosbahi_381.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00158906, version 1

Collections

Citation

Olfa Mosbahi, Jacques Jaray. Specification and Proof of Liveness Properties in B Event Systems. Joaquim Filipe and Boris Shishkov and Markus Helfert. 2nd International Conference on Software and Data Technologies - ICSOFT 2007, Jul 2007, Barcelone, Spain. INSTICC Press, pp.25-34, 2007. 〈inria-00158906〉

Partager

Métriques

Consultations de la notice

474

Téléchargements de fichiers

143