A Formal Model of the UML Metamodel: The UML State Machine and Its Integrity Constraints
(2002)DOI: http://dx.doi.org/10.1007/3-540-45648-1\_26
Abstract
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.