Skip to Main content Skip to Navigation
Conference papers

Creating sequential programs from Event-B models

Abstract : Event-B is an emerging formal method with good tool support for various kinds of system modelling. However, the control flow in Event-B consists only of non-deterministic choice of enabled events. In many applications, notably in sequential program construction, more elaborate control flow mechanisms would be convenient. This paper explores a method, based on a scheduling language, for describing the flow of control. The aim is to be able to express schedules of events; to reason about their correctness; to create and verify patterns for introducing correct control flow. The conclusion is that using patterns, it is feasible to derive efficient sequential programs from event-based specifications in many cases.
Complete list of metadata
Contributor : Ist Inria Nancy Grand Est Connect in order to contact the contributor
Submitted on : Monday, October 11, 2010 - 11:48:35 AM
Last modification on : Monday, October 11, 2010 - 11:48:35 AM


  • HAL Id : inria-00522651, version 1



Pontus Boström. Creating sequential programs from Event-B models. Integrated Formal Methods - IFM 2010, INRIA Nancy Grand Est, Oct 2010, Nancy, France. ⟨inria-00522651⟩



Record views