Generic Instantiation

Event-B lacks the ability to instantiate and reuse generic developments in other formal developments. We propose a way of instantiating generic models and extending the instantiation to a chain of refinements. We define sufficient proof obligations to ensure that the proofs associated to a generic development remain valid in an instantiated development thus avoiding re-proofs.

The instances inherit properties from the generic development (pattern) and are parameterised by renaming/replacing those properties to specific instance element names. Proof obligations are generated to ensure that assumptions used in the pattern are satisfied in the instantiation. In that sense our approach avoids re-proof of pattern proof obligations in the instantiation. The reusability of a development is expressed by instantiating a development (pattern) according to a more specific problem.

The proposal (from the University of Southampton) is as follows: File:Generic Instantiation Proposal.pdf.

A Generic Instantiation tool is developed for Event-B by the University of Southampton. See Generic Instantiation Plug-in User Guide.

Another generic instantiation tool is developed by Hitachi Ltd. and ETH Zurich. See Generic Instantiation User Guide.

The University of Southampton, Hitachi Ltd. and ETH Zurich are discussing on how to consolidate the work and merge the two plug-ins.