Derivation of algorithmic control structures in Event-B refinement

Sadegh Dalvandi, Michael Butler & Abdolbaghi Rezazadeh
Abstract: The Event-B formalism allows program specifications to be modelled at an abstract level and refined towards a concrete model. However, Event-B lacks explicit control flow structure and ordering is implicitly encoded in event guards. This makes it difficult to identify and apply rules for transformation of Event-B models to sequential code. This paper introduces a scheduling language to support the incremental derivation of algorithmic control structure for events as part of the Event-B refinement process. We provide intermediate control structures for non-deterministic iteration and choice that ease the transition from abstract specifications to sequential implementations. We present rules for transforming algorithmic structures to more concrete refinements. We illustrate our approach by applying our method to the Schorr–Waite graph marking algorithm.

The paper can be downloaded from here.

The fully verified Event-B model of the Schorr-Waite graph marking algorithm can be downloaded from here.