A formal semantics for UML interactions

The UML abstract syntax and semantics specification distinguishes between the statics and the dynamics of collaborations: the role context and interactions. We propose a formal semantics of interactions based on the abstract syntax and directly reflecting the specification. The semantics is both parametric in the notion of context and in semantic details that are intentionally left open by the specification, but resolves true inconsistencies. The formalisation uses temporal logic formulae in the style of Manna and Pnueli. We illustrate the flexibility of our semantics by discussing instantiations for a running example; its intuitiveness is substantiated by proving that the temporal formulae give rise to partial orders that also directly can be inferred from interactions.