Decomposition is a technique to separate the design of a complex system into smaller sub-models, which improves scalability and team development. In the shared-variable decomposition approach for Event-B sub-models share external variables and communicate through external events which cannot be easily refined. Our first contribution hence is a proposal for a new construct called interface that encapsulates the external variables, along with a mechanism for interface instantiation. Using the new construct and mechanism, external variables can be refined consistently. Our second contribution is an approach for verifying the correctness of Event-B extensions using the supporting Rodin tool. We illustrate our approach by proving the correctness of interface instantiation. © 2012 Springer-Verlag.
CITATION STYLE
Hallerstede, S., & Hoang, T. S. (2012). Refinement by interface instantiation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7316 LNCS, pp. 223–237). https://doi.org/10.1007/978-3-642-30885-7_16
Mendeley helps you to discover research relevant for your work.