Supporting Reuse of Event-B Developments through Generic Instantiation

It is believed that reusability in formal development should reduce the time and cost of formal modelling within a production environment. Along with the ability to reuse formal models, it is desirable to avoid unnecessary re-proof when reusing models. Event-B is a formal method that allows modelling and refinement of systems. Event-B supports generic developments through the context construct. Nevertheless 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. Key words: formal methods, event-B, reusability, generic instantiation

• Type: Conference
• Year: 2009
• Where: ICFEM
• Authors: Renato Silva, Michael Butler
• Keywords: Formal Developments, Formal Methods, Generic Development, ICFEM 2009, Software Engineering