Modelling concurrent interactions

In UML 2.0 sequence diagrams have been considerably extended but their expressiveness and semantics remains problematic in several ways. In other work we have shown how sequence diagrams combined with an OCL liveness template gives us a much richer language for inter-object behaviour specification. In this paper, we give a semantics of these enriched diagrams using labelled event structures. Further, we show how sequence diagrams can be embedded into a true-concurrent two-level logic interpreted over labelled event structures. The top level logic, called communication logic, is used to describe inter-object specification, whereas the lower level logic, called home logic, describes intra-object behaviour. An interesting consequence of using this logic relates to how state-based behaviour can be synthesised from inter-object specifications. Plans of extending the Edinburgh Concurrency Workbench in this context are discussed.