Where academic tradition
meets the exciting future

Visual Component-Based Development of Formal Models

Sergey Ostroumov, Marina Waldén, Visual Component-Based Development of Formal Models. In: Mira Kajko-Mattsson, Pål Ellingsen, Paolo Maresca (Eds.), The Third International Conference on Advances and Trends in Software Engineering (SoftEng), 43–50, IARIA, 2017.


Formal methods, such as Event-B provide a means for system-level specification and verification supported by correctness proofs. However, the formal Event-B specification of a system requires background knowledge, which prevents a fruitful communication between the developer and the customer. In addition, scalability and reusability are limiting factors in using formal methods, such as Event-B in complex system development. This paper presents an approach to facilitate scalability of formal development in Event-B. Our aim is 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 that eases the rigorous development by applying the “drag-and-drop” approach and enhances the communication between a developer and a customer. We present a subset of components from the digital hydraulics domain and outline the compositionality mechanism.

BibTeX entry:

  title = {Visual Component-Based Development of Formal Models},
  booktitle = {The Third International Conference on Advances and Trends in Software Engineering (SoftEng)},
  author = {Ostroumov, Sergey and Waldén, Marina},
  editor = {Kajko-Mattsson, Mira and Ellingsen, Pål and Maresca, Paolo},
  publisher = {IARIA},
  pages = {43–50},
  year = {2017},
  ISSN = {2519-8394},

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Edit publication