Formal Library of Visual Components

Scalability and reusability are the limiting factors in using formal methods such as Event-B in complex system development. In addition, the formal Event-B specification of a system requires background knowledge, which prevents a fruitful communication between the developer and the customer. On the other hand, the formal development in Event-B provides a means for system-level specification and verification supported by the correctness proof. 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 the 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. Event-B also has a mature tool support, namely the Rodin platform, which generates and attempts to automatically discharge the necessary proof obligations. This paper presents an approach which is to facilitate scalability of formal development in Event-B. We aim to build a formal library of parameterized visual components that can be reused whenever needed. Each component is formally developed and proved correct by utilizing the advantages of Event-B. Furthermore, each component has a unique graphical representation which eases the rigorous development process by applying the “drag-and-drop” approach and enhances the communication between a developer and a customer. We present a subset of components from different application domains.