کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
435045 | 1441672 | 2014 | 20 صفحه PDF | دانلود رایگان |
• A limited form of refinement called interface instantiation is proposed for the Event-B formalism.
• Interface instantiation equips Event-B with a technique for shared-variable refinement.
• Interface instantiation fits seamlessly with Event-B decomposition and refinement.
• A worked out example is used to demonstrate this.
• A correctness proof is provided.
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.
Journal: Science of Computer Programming - Volume 94, Part 2, 15 November 2014, Pages 144–163