SPECIFICATION AND PROOF OF LIVENESS PROPERTIES IN B EVENT SYSTEMS

Olfa Mosbahi, Jacques Jaray

2007

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.

Paper Citation

in Harvard Style

Mosbahi O. and Jaray J. (2007). SPECIFICATION AND PROOF OF LIVENESS PROPERTIES IN B EVENT SYSTEMS . In Proceedings of the Second International Conference on Software and Data Technologies - Volume 2: ICSOFT, ISBN 978-989-8111-06-7, pages 25-34. DOI: 10.5220/0001342400250034

in Bibtex Style

@conference{icsoft07,
author={Olfa Mosbahi and Jacques Jaray},
title={SPECIFICATION AND PROOF OF LIVENESS PROPERTIES IN B EVENT SYSTEMS},
booktitle={Proceedings of the Second International Conference on Software and Data Technologies - Volume 2: ICSOFT,},
year={2007},
pages={25-34},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0001342400250034},
isbn={978-989-8111-06-7},
}

in EndNote Style

TY - CONF
JO - Proceedings of the Second International Conference on Software and Data Technologies - Volume 2: ICSOFT,
TI - SPECIFICATION AND PROOF OF LIVENESS PROPERTIES IN B EVENT SYSTEMS
SN - 978-989-8111-06-7
AU - Mosbahi O.
AU - Jaray J.
PY - 2007
SP - 25
EP - 34
DO - 10.5220/0001342400250034