A Situation Calculus-based semantic framework for UML

A recent trend in the study of UML formal semantics is to integrate semantics of various UML diagrams into a single framework. The aim is to get a unified basis for main research topics like validation, verification and syntax checking. In this paper, we propose an approach based on the Situation Calculus (SC) which is a sophisticated action theory and is capable of modeling general systems. UML models are treated as a tailored SC system, containing eternals, fluents and actions that formalize the frequently used concepts in the UML metamodel. Class diagrams and object diagrams are modeled by eternals for consistency checking. State machine diagrams and sequence diagrams are modeled by fluents and actions, with corresponding precondition axioms and successor state axioms in SC. We use Golog, an executable high-level programming language based on the SC, to analyze and test UML diagrams. Based on the methods proposed in this paper, UML diagrams can be formally analyzed and simulated in the Golog interpreter, which can be useful in discovering system deficits at the design level.