Checking Consistency in UML Diagrams: Classes and State Machines

  • Holger Rasch
  • Heike Wehrheim
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2884)


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.


State Machine Semantic Model Basic Consistency Class Elevator External Choice 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 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
  2. 2.
    Bowman, H., Steen, M.W.A., Boiten, E.A., Derrick, J.: A formal framework for viewpoint consistency. Formal Methods in System Design 21, 111–166 (2002)CrossRefzbMATHGoogle Scholar
  3. 3.
    Davies, J., Crichton, C.: Concurrency and Refinement in the Unified Modeling Language. Electronic Notes in Theoretical Computer Science, 70(3) (2002)Google Scholar
  4. 4.
    Derrick, J., Boiten, E.: Refinement in Z and Object-Z. Foundations and Advanced Application. Springer, Heidelberg (2001)CrossRefzbMATHGoogle Scholar
  5. 5.
    Engels, G., Heckel, R., Küster, J.: Rule-based Specification of Behavioral Consistency based on the UML Meta-Model. In: Gogolla, M. (ed.) UML 2001. LNCS, vol. 2185, p. 272. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  6. 6.
    Engels, G., Heckel, R., Küster, J.M., Groenewegen, L.: Consistency-preserving model evolution through transformations. In: Jézéquel, J.-M., Hussmann, H., Cook, S. (eds.) UML 2002. LNCS, vol. 2460, pp. 212–226. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  7. 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. 8.
    Farooqui, K., Logrippo, L.: Viewpoint Transformation. In: Proc. of the International Conference on Open Distributed Processing, pp. 352–562 (1993)Google Scholar
  9. 9.
    Fischer, C.: CSP-OZ: A combination of Object-Z and CSP. In: Bowman, H., Derrick, J. (eds.) Formal Methods for Open Object-Based Distributed Systems (FMOODS 1997), vol. 2, pp. 423–438. Chapman and Hall, Boca Raton (1997)CrossRefGoogle Scholar
  10. 10.
    Fischer, C., Hallerstede, S.: Data-Refinement in CSP-OZ. Technical Report TRCF-97-3, University of Oldenburg (June 1997)Google Scholar
  11. 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. 12.
    Formal Systems (Europe) Ltd. Failures-Divergence Refinement: FDR2 User Manual (October 1997)Google Scholar
  13. 13.
    Francez, N.: Fairness. Texts and Monographs in Computer Science. Springer, Heidelberg (1986)CrossRefzbMATHGoogle Scholar
  14. 14.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)zbMATHGoogle Scholar
  15. 15.
    Josephs, M.B.: A state-based approach to communicating processes. Distributed Computing 3, 9–18 (1988)CrossRefzbMATHGoogle Scholar
  16. 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
  17. 17.
    Lehmann, D., Pnueli, A., Stavi, J.: Impartiality, Justice and Fairness: The Ethics of Concurrent Termination. In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol. 115, pp. 264–277. Springer, Heidelberg (1981)CrossRefGoogle Scholar
  18. 18.
    Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)Google Scholar
  19. 19.
    Smith, G.: The Object-Z Specification Language. Kluwer Academic Publishers, Dordrecht (2000)CrossRefzbMATHGoogle Scholar
  20. 20.
    Smith, G., Derrick, J.: Refinement and verification of concurrent systems specified in Object-Z and CSP. In: Hinchey, M., Liu, S. (eds.) Int. Conf. of Formal Engineering Methods (ICFEM), pp. 293–302. IEEE, Los Alamitos (1997)CrossRefGoogle Scholar
  21. 21.
    OMG Unified Modeling Language specification, version 1.5 (March 2003),

Copyright information

© IFIP International Federation for Information Processing 2003

Authors and Affiliations

  • Holger Rasch
    • 1
  • Heike Wehrheim
    • 1
  1. 1.Department InformatikUniversität OldenburgOldenburgGermany

Personalised recommendations