Facilitating Formal Event-B Development by Visual Component-based Design

Due to the ever increasing complexity and criticality of modern systems, their correctness has to be evidently shown. This can be achieved by the use of formal methods such as Event-B. The development in Event-B follows the refinement approach, in which the specification is created top-down starting from a non-deterministic model and ending in a precise implementable one. The specification process is supported by theorem proving, so that one can guarantee correctness of the specification with respect to postulated properties called invariants. On the other hand, the formal modelling is limited in terms of reusability and bottom-up scalability. In addition, the formal Event-B specification of a system requires background knowledge, which prevents a fruitful communication between the developer and the customer.

This paper presents an approach that aims to facilitate scalability and reusability of formal development in Event-B as well as to enhance communication between the developer and the customer. The approach relies on the component-based design, where each component has a specific graphical representation. We present a set of the refinement patterns which support scalability and provide the connectivity (composition) between the components following the refinement approach. Our goal is to merge the top-down (refinement) and bottom-up (component-based development) approaches in order to improve rigorous Event-B specifications by visual representation. Eventually, the developers obtain the specification of a system that consists of two layers: logical and visual. The logical layer is fully based on the Event-B mathematical engine which gives the correctness proof. The visual layer is added on top of the logical layer, which gives a graphical representation of the Event-B specification.