Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata

Cited literature [10 references]  Display  Hide  Download
Contributor : Olfa Mosbahi Connect in order to contact the contributor
Submitted on : Monday, July 2, 2007 - 12:15:08 AM
Last modification on : Friday, February 4, 2022 - 3:30:46 AM
Long-term archiving on: : Monday, September 24, 2012 - 10:46:54 AM


Files produced by the author(s)


  • HAL Id : inria-00158906, version 1



Olfa Mosbahi, Jacques Jaray. Specification and Proof of Liveness Properties in B Event Systems. 2nd International Conference on Software and Data Technologies - ICSOFT 2007, INSTICC - Institute for Systems and Technologies of Information, Control and Communication, Jul 2007, Barcelone, Spain. pp.25-34. ⟨inria-00158906⟩



Record views


Files downloads