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

https://hal.inria.fr/inria-00158906
Contributor : Olfa Mosbahi <>
Submitted on : Monday, July 2, 2007 - 12:15:08 AM
Last modification on : Friday, February 26, 2021 - 3:28:05 PM
Long-term archiving on: : Monday, September 24, 2012 - 10:46:54 AM

File

mosbahi_381.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00158906, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

524

Files downloads

223