Evaluation of Graphical Control Flow Management Approaches for Event-B Modelling

Abstract

Integrating graphical representations with formal methods can help bridge the gap between requirements and formal modelling. In this paper, we compare and evaluate two graphical approaches aiming at describing control flows and refinement in Event-B, and we use a fire dispatch system case study to perform this evaluation. The fire dispatch system case study provides a good example of a complex workflow through which we try to identify a process that facilitates defining the structural and the behavioural parts of the Event-B model. In our case study, we focus on building the dynamic part of the model to evaluate the two diagrammatic notations: UML Activity Diagrams and Atomicity Decomposition Diagrams. Based on our evaluation, we try to identify the advantages and limitations of both approaches. Finally, we try to compare how both graphical notations can affect the Event-B formal modelling of our case study.