Consistency Check of Class Diagram and Sequence Diagrams Using B-Method

This paper proposes a systematic mean of consistency check for UML class diagram and its related sequence diagrams representing the critical scenarios using B-Method. The B-Method is a formal specification modeling which is used to describe the semantics of system in terms of mathematical notations – set theory and first-order predicate logic. In our approach, a class diagram and its related sequence diagrams are formally translated into B Abstract Machine (BAM) using a set of our translation rules. Our translation rules generate the semantics of both structural and behavioral properties of the UML class diagram and sequence diagrams.

            This paper focuses on two parts. Firstly, the formalization of the UML class diagram – a collection of classes and their relations such as association, aggregation, composition, generalization or inheritance, is investigated and defined for the structural property. Secondly, the formalization of UML sequence diagrams – a collection of scenarios which illustrate the major interactions between related classes as to achieve a specific goal, is defined for the behavioral property and verified against their original structure in class diagram. Moreover, we finally define the complex operations within the critical sequence diagrams by exploiting the calling-called dependency between class operations from Hung Ledang’s work. The formal specification in BAM is finally generated and verified by B-Toolkit.

 Keywords: UML, Class Diagram, Sequence Diagrams, B-Method, Formal Specifications Modeling, B Abstract Machine

 Corresponding author: E-mail: Waitaya.S@Student.chula.ac.th. , wiwat@chula.ac.th