On the Semantics of UML/MARTE Clock Constraints

The UML goal of being a general-purpose modeling language discards the possibility to adopt too precise and strict a semantics. Users are to refine or define the semantics in their domain specific profiles. In the UML profile for MARTE, we devised a broadly expressive time model to provide a generic timed interpretation for UML models. Our clock constraint specification language supports the specification of systems with multiple clock domains. Starting with a priori independent clocks, we progressively constrain them to get a family of possible executions. Our language supports both synchronous and asynchronous constraints, just like the synchronous language Signal, but also allows explicit non determinism. In this paper, we give a formal semantics to a core subset of MARTE clock constraint language and we give an equivalent interpretation of this kernel in two other very different formal languages, Signal and time Petri nets.