Checking Consistency in UML Diagrams: Classes and State Machines
One of the main advantages of the UML is its possibility to model different views on a system using a range of diagram types. The various diagrams can be used to specify different aspects, and their combination makes up the complete system description. This does, however, always pose the question of consistency: it may very well be the case that the designer has specified contradictory requirements which can never be fulfilled together.
In this paper, we study consistency problems arising between static and dynamic diagrams, in particular between a class and its associated state machine. By means of a simple case study we discuss several definitions of consistency which are based on a common formal semantics for both classes and state machines. We furthermore show how consistency checks can be automatically carried out by a model checker. Finally, we examine which of the consistency definitions are preserved under refinement.
KeywordsState Machine Semantic Model Basic Consistency Class Elevator External Choice
- 1.Bernardeschi, C., Dustzadeh, J., Fantechi, A., Najm, E., Nimour, A., Olsen, F.: Transformations and Consistent Semantics for ODP Viewpoints. In: Proceedings of Second IFIP conference on Formal Methods for Open Object-based Distributed Systems - FMOODS 1997. Chapman and Hall, Sydney (1997)Google Scholar
- 3.Davies, J., Crichton, C.: Concurrency and Refinement in the Unified Modeling Language. Electronic Notes in Theoretical Computer Science, 70(3) (2002)Google Scholar
- 7.Engels, G., Küster, J., Heckel, R., Groenewegen, L.: A Methodology for Specifying and Analyzing Consistency of Object-Oriented Behavioral Models. In: 9th ACM Sigsoft Symposium on Foundations of Software Engineering. ACM Software Engineering Notes, vol. 26 (2001)Google Scholar
- 8.Farooqui, K., Logrippo, L.: Viewpoint Transformation. In: Proc. of the International Conference on Open Distributed Processing, pp. 352–562 (1993)Google Scholar
- 10.Fischer, C., Hallerstede, S.: Data-Refinement in CSP-OZ. Technical Report TRCF-97-3, University of Oldenburg (June 1997)Google Scholar
- 11.Fischer, C., Wehrheim, H.: Model-checking CSP-OZ specifications with FDR. In: Araki, K., Galloway, A., Taguchi, K. (eds.) Proceedings of the 1st International Conference on Integrated Formal Methods (IFM), pp. 315–334. Springer, Heidelberg (1999)Google Scholar
- 12.Formal Systems (Europe) Ltd. Failures-Divergence Refinement: FDR2 User Manual (October 1997)Google Scholar
- 16.Kuzniarz, L., Reggio, G., Sourrouille, J.L., Huzar, Z. (eds.): UML 2002 – Workshop on Consistency Problems in UML-based Software Development, volume 06 of Blekinge IOT Research Report (2002)Google Scholar
- 18.Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)Google Scholar
- 21.OMG Unified Modeling Language specification, version 1.5 (March 2003), http://www.omg.org