Equivalence of denotational and operational semantics for interaction languages
Abstract
Message Sequence Charts (MSC) and Sequence Diagrams (SD) are graphical models that represent the behaviours of distributed and concurrent systems via the scheduling of discrete emission and reception events. In order to exploit them as support for formal methods, a mathematical semantics is required. In the literature, two kinds of semantics are classically proposed: denotational semantics, well suited to reason about algebraic properties and operational semantics, well suited to be the basis of verification algorithms. We define an algebraic language to specify so-called interactions, similar to the MSC and SD models. This language is equipped with a denotational semantics associating a set of traces (sequences of observed events) to each interaction. We then define a structural operational semantics in the style of process algebras and formally prove the equivalence of the two semantics.