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

Article Sidebar

PDF
Published: Mar 30, 2018
Keywords:
UML, Class Diagram, Sequence Diagrams, B-Method, Formal Specifications Modeling, B Abstract Machine

Main Article Content

Waitaya Sricharunrat*
Department of Computer Engineering, Faculty of Engineering, Chulalongkorn University, Bangkok, Thailand.
Wiwat Vatanawood
Department of Computer Engineering, Faculty of Engineering, Chulalongkorn University, Bangkok, Thailand.

Abstract

 


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


 

Article Details

Issue
Vol. 6 No. 2a (2006)
Section
Original Research Articles

Copyright Transfer Statement

 The copyright of this article is transferred to Current Applied Science and Technology journal with effect if and when the article is accepted for publication. The copyright transfer covers the exclusive right to reproduce and distribute the article, including reprints, translations, photographic reproductions, electronic form (offline, online) or any other reproductions of similar nature.

 The author warrants that this contribution is original and that he/she has full power to make this grant. The author signs for and accepts responsibility for releasing this material on behalf of any and all co-authors.

Here is the link for download: Copyright transfer form.pdf

 

 

References

[1] Abrial. J-R. 1996 The B – Book Assigning Programs to Meanings. Cambridge University Press.
[2] Grady Booch, Jame Rumbaugh and Ivar Jacobson. 1998 The Unified Modeling Language User Guide. Addison Wesley.
[3] Arlow, J., Neustadt. 1.,2002 UML and The Unified Process Practical Object – Oriented Analysis and Design. Addison Wesley.
[4] Ledang, H. and Souquières, J. 2001 Integrating UML and B Specification Techniques. Workshop at Informatik, 2001.
[5] Ledang, H. and Souquières, J. 2001 Modeling Class Operations in B: a case study on the pump component. Technical Report A01-R-011. Laboratory Lorrian de Recherche en Informatique et ses Applications, 2001.
[6] Lano, K. and Haughton, H. 1996 Specification in B: An introduction using the B Toolkit. Imperial College Press.