Checking Consistency of UML state and sequence diagrams using B
Résumé
The development of software systems using UML, the Unified Modelling Language, necessitates the construction of different models from different point of views with overlapping UML diagrams. This leads important to ensure that the behaviour of the different produced models is consistent. This task is difficult to accomplish manually, in particular for complex systems and UML existing tools provide unsatisfactory support for maintaining the consistency between the different diagrams. In this paper, we focus on sequence diagrams and protocol state machines, which provide a graphical notation for describing dynamic aspects of system behaviour. We check the consistency between these two diagrams, taking advantages from the use of the B formal method and its support tools. We execute sequence diagrams in the B world and verify that they correspond to legal sequence of operation calls and that they do not conflict with safety and dynamic properties. Our proposition is illustrated by a simplified case study, the access control of persons to a building.