
Open access
Date
2012Type
- Report
ETH Bibliography
yes
Altmetrics
Abstract
Abstract Event-B has given developers the opportunity to construct models of complex systems that are correct by construction. However, there is no systematic approach, especially in terms of reuse, 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 subproblem. As a result, we can use patterns to construct a model which can subsequently be used as a pattern to construct a arger model. We also present the interaction between develdevelopers and the tool support within the associated RODIN Platform of Event-B. The approach has been applied successfully to some medium-size industrial case studies. Show more
Permanent link
https://doi.org/10.3929/ethz-a-007224905Publication status
publishedPublisher
Eidgenössische Technische Hochschule ZürichSubject
SPECIFICATION LANGUAGES (COMPUTER SYSTEMS); Model reuse; Event-B,; Formal modelling; SPEZIFIKATIONSSPRACHEN (COMPUTERSYSTEME); Design patterns; SYSTEMS ANALYSIS + SYSTEMS DEVELOPMENT + SYSTEMS DESIGN (COMPUTER SYSTEMS); Formal methods,; SYSTEMANALYSE + SYSTEMENTWICKLUNG + SYSTEMENTWURF (COMPUTERSYSTEME)Organisational unit
02150 - Dep. Informatik / Dep. of Computer Science
Notes
Technical Reports D-INFK.More
Show all metadata
ETH Bibliography
yes
Altmetrics