Qualitative Software Engineering and Event-B Modeling for Communication and Use Case Diagrams

Abstract

Now a days distributed and parallel applications are most popular because of their wide usage and advantages. Some of the applications like telecommunications and aircraft systems have many interactions between their sub-systems in order to fulfil the requirements which include complex computations and calculations in them. It is very important to define the exact properties and features of these systems along with the workflow. Unified Modeling language provides a great opportunity of modelling complex applications like these by defining the structure, flow and the work topologies of the distributed applications. But inspite of having wide range of usage, UML lacks in providing the detailed semantics of the various subsystems in these distributed applications which indeed is important in defining the exact features of them. In this paper, we will understand the importance of implementation of specifications using formal methods like event-B through a simple example and verify its results using ProB. Later, we have defined the UML diagrams like use case and communication diagrams in various scenarios and have performed the Event B modeling for these examples.