Tool Support for Event-B Code Generation
Andrew J. F. Edmunds, Michael J. Butler · ePrints Soton (University of Southampton) · 2010
The Event-B method is a formal approach to modelling systems, using refi?nement. Initial specifi?cation is done at a high level of abstraction; detail is added in refi?nement steps as the development proceeds toward implementation. In previous work we developed an approach to bridge the gap between abstract specifi?cations and implementations using an implementation level specifi?cation notation. In this paper we present details of the tool support for our notation and some of our experiences using the tool.