B événementiel et les propriétés de vivacité

Olfa Mosbahi 1 Jacques Jaray 1
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper deals with the verification of liveness properties on reactive systems. We are based on the event B method to specify and validate such systems. By considering the limitation of the B to invariance properties, we propose to apply the language TLA+ to verify liveness properties on a software behavior. We extend, in particular, the expressivity and the semantics of the event B method to deal with the specification n of fairness and eventuality properties. By transforming an extended B model into TLA+ module by using a prototype system (B2TLA+) that we have developed, we can verify these properties thanks to the modelchecker TLC on finite state systems. For the verification of infinite-state systems, we propose the use of predicate diagrams.
Document type :
Journal articles
Complete list of metadatas

Contributor : Dominique Méry <>
Submitted on : Saturday, March 26, 2011 - 11:07:34 AM
Last modification on : Tuesday, April 24, 2018 - 1:53:16 PM

Links full text




Olfa Mosbahi, Jacques Jaray. B événementiel et les propriétés de vivacité. Journal Européen des Systèmes Automatisés (JESA), Lavoisier, 2010, 44 (9-10), pp.1119-1163. ⟨10.3166/jesa.44.1119-1163⟩. ⟨inria-00580131⟩



Record views