An incremental development of the Mondex system in Event-B
Formal Aspects of Computing, 20 (1):
61--77 (January 2008)DOI: http://dx.doi.org/10.1007/s00165-007-0061-4
Abstract
Abstract A development of the Mondex system was undertaken using Event-B and its associated proof tools. An incremental approach was used whereby the refinement between the abstract specification of the system and its detailed design was verified through a series of refinements. The consequence of this incremental approach was that we achieved a very high degree of automatic proof. The essential features of our development are outlined. We also present some modelling and proof guidelines that we found helped us gain a deep understanding of the system and achieve the high degree of automatic proof.
