Refinement and Reachability in Event_B

Abstract : Since the early 90's (after the seminal article of R. Back [4]), the refinement of stuttering steps [5] are performed by means of new actions (called here events) refining skip. It is shown in this article that such a refinement method is not always possible in the development of large systems. We shall instead use events refining some kind of non-deterministic actions maintaining the invariant (sometimes called keep). We show that such new refinements are completely safe. In a second part, we explain how such a mechanism can be used to express some reachability conditions that were otherwise expressed using some special temporal logic statements à la TLA [5] in a previous article [2]. Examples will be used to illustrate our proposals.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00001245
Contributor : Publications Loria <>
Submitted on : Tuesday, April 11, 2006 - 5:38:31 PM
Last modification on : Thursday, September 19, 2019 - 5:00:04 PM

Links full text

Identifiers

Collections

Citation

Jean-Raymond Abrial, Dominique Cansell, Dominique Méry. Refinement and Reachability in Event_B. ZB 2005 : Formal Specification and Development in Z and B : 4th International Conference of B and Z Users, Apr 2005, Guilford/UK, pp.222-241, ⟨10.1007/11415787_14⟩. ⟨inria-00001245⟩

Share

Metrics

Record views

238