A Formal Model of the UML Metamodel: The UML State Machine and Its Integrity Constraints

  • Soon-Kyeong Kim
  • David Carrington
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2272)


This paper presents a formal Object-Z model of the UML State Machine. We encapsulate the abstract syntax and the static and dynamic semantics for each individual model construct as a single Object-Z class. To formalize the dynamic semantics, a denotational semantics of the construct is given first ignoring detailed operational sequences. Based on this denotational semantics, an operational (execution) semantics is then defined in terms of (Object-Z) class operations and invariants constraining the operation sequences. The timed refinement calculus is used to define the operation sequences within Object-Z. Finally, integrity consistency constraints with other model constructs are formalized in terms of invariants defined in the state machine. Our approach not only enhances the precision of the UML state machine description but also overcomes the lack of modularity, extensibility and reusability of the current UML semantic representation.


State Machine Unify Modeling Language Operational Semantic Abstract Syntax Composite State 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    T. Clark, A. Evans, R. France, S. Kent, and B. Rumpe, Response to UML 2.0 Request for Information, 1999. available at
  2. [2]
    B. P. Douglass, Real-Time UML: Developing Efficient Objects for embedded systems, Addison-Wesley, 1998.Google Scholar
  3. [3]
    R. Duke and R. Gordon, Formal Object-Oriented Specification Using Object-Z, Macmillan, 2000.Google Scholar
  4. [4]
    Evans and S. Kent, Core meta modelling semantics of UML: The pUML approach, Proc. UML’99, LNCS. No. 1723, pp. 140–155, 1999.Google Scholar
  5. [5]
    R. France, A. Evans, K. Lano, and B. Rumpe, Developing the UML as a Formal Modeling Notation, Computer Standards and Interfaces, No. 19, pp. 325–334, 1998.Google Scholar
  6. [6]
    D. Harel and A. Naamad, The STATEMATE semantics of Statecharts, ACM Transaction on Software Engineering, vol. 5, pp 293–333, 1996.CrossRefGoogle Scholar
  7. [7]
    Henderson-Sellers and F. Barbier, Black and White Diamonds, Proc UML’99, LNCS, No. 1723, pp. 550–565, 1999.Google Scholar
  8. [8]
    S-K. Kim and D. Carrington, Formalizing the UML class diagram using Object-Z, Proc. UML’99, LNCS, No. 1723, pp. 83–98, 1999.Google Scholar
  9. [9]
    S-K. Kim and D. Carrington, A Formal Mapping between UML Models and Object-Z Specifications, ZB2000, LNCS, No. 1878, pp. 2–21, 2000.Google Scholar
  10. [10]
    S-K. Kim and D. Carrington, UML Metamodel Formalization with Object-Z: the State Machine package, SVRC technical Report 00-29, The University of Queensland, 2000.Google Scholar
  11. [11]
    S-K. Kim and D. Carrington, A Formal Denotational Semantics of UML in Object-Z, the special issue of the journal of l’Objet, Vol. 7(1), 2001.Google Scholar
  12. [12]
    G. Kwon, Rewrite Rules and Operational Semantics for Model Checking UML statecharts, Proc. UML’2000, LNCS, No. 1939, pp. 528–540, 2000.Google Scholar
  13. [13]
    Latella, I. Majzik, and M. Massink, Towards a formal operational semantics of UML statechart diagrams, In 3rd International Conference on Formal Methods for Open Object-Oriented Distributed Systems(FMOODS), Kluwer, 1999.Google Scholar
  14. [14]
    J. Lilius and I. P. Paltor, Formalizing UML state machines for model checking, Proc. UML’99, LNCS, No. 1723, pp. 430–445, 1999.Google Scholar
  15. [15]
    OMG, Unified Modeling Language Specification, version 1.3, 1999,
  16. [16]
    OMG, Response to OMG RFP ad/98-11-01: Action Semantics for the UML, 2000. Available at
  17. [17]
    G. Reggio, E. Astesiano, C. Choppy, and H. Hussmann, Analysing UML Active Classes and Associated State Machines-Lightweight Formal Approach, Proc. FASE 2000, LNCS. No.1783, pp. 127–146. Springer Verlag, 2000.Google Scholar
  18. [18]
    M. Richters and M. Gogolla, On formalizing the UML Object Constraint Language OCL, Proc. 17th Int. Conf. Conceptual Modeling, LNCS. No. 1507, pp. 449–464, 1998.Google Scholar
  19. [19]
    G. Smith and I. Hayes, Structuring Real-Time Object-Z Specifications, IFM’2000, LNCS, No. 1945, pp. 97–115, 2000.Google Scholar
  20. [20]
    G. Smith. The Object-Z Specification Language. Advances in Formal Methods. Kluwer Academic Publishers, 2000.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Soon-Kyeong Kim
    • 1
  • David Carrington
    • 1
  1. 1.School of Computer Science and Electrical EngineeringThe University of QueenslandBrisbaneAustralia

Personalised recommendations