Refinement and Reachability in Event_B

http//www.springerlink.comSince 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