creators_name: Hoang, Thai Son creators_name: Fürst, Andreas creators_name: Abrial, Jean-Raymond creators_id: htson@inf.ethz.ch creators_id: andreas.fuerst@inf.ethz.ch creators_id: jabrial@inf.ethz.ch type: article datestamp: 2010-02-05 10:29:56 lastmod: 2010-02-05 10:29:56 metadata_visibility: show title: Event-B Patterns and Their Tool Support ispublished: pub subjects: deploy_method_comp full_text_status: none abstract: Event-B has given developers the opportunity to construct models of complex systems which are correct by construction. However, there is no systematic approach, especially in terms of reusing, which could help with the construction of these models. We introduce the notion of design patterns within the framework of Event-B to shorten this gap. Our approach preserves the correctness of the models which is critical in formal methods and also reduces the proving effort. Within our approach, an Event-B design pattern is just another model devoted to the formalisation of a typical sub-problem. As a result, we can use patterns to construct a model which can subsequently be used as a pattern to construct a larger model. We also present the interaction between developers and the future tool support within the associated Rodin Platform of Event-B. The approach has been applied successfully in some medium-size industrial case studies. date: 2009-11 date_type: published publication: 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods publisher: IEEE Computer Society pagerange: 210-219 refereed: TRUE official_url: http://doi.ieeecomputersociety.org/10.1109/SEFM.2009.17 citation: Hoang, Thai Son and Fürst, Andreas and Abrial, Jean-Raymond (2009) Event-B Patterns and Their Tool Support. 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods . pp. 210-219.