Formal Library of Visual Components

Sergii Ostroumov, Marina Walden

Research output: Book/Journal/ReportCommissioned reportProfessional


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.
Original languageEnglish
PublisherTurku Centre for Computer Science (TUCS)
ISBN (Print)978-952-12-3310-4
Publication statusPublished - 2015
MoE publication typeD4 Published development or research report or study

Publication series

NameTUCS Technical Report


Dive into the research topics of 'Formal Library of Visual Components'. Together they form a unique fingerprint.

Cite this