Title: Equivalence of Denotational and Operational Semantics for Interaction Languages
Abstract: Message Sequence Charts (MSC) and Sequence Diagrams (SD) are graphical models representing the behaviours of distributed and concurrent systems via the scheduling of discrete emission and reception events. So as to exploit them in formal methods, a mathematical semantics is required. In the literature, different kinds of semantics are proposed: denotational semantics, well suited to reason about algebraic properties and operational semantics, well suited to establish verification algorithms. We define an algebraic language to specify so-called interactions, similar to the MSC and SD models. It is equipped with a denotational semantics associating sets of traces (sequences of observed events) to interactions. We then define a structural operational semantics in the style of process algebras and prove the equivalence of the two semantics.
Publication Year: 2022
Publication Date: 2022-01-01
Language: en
Type: book-chapter
Indexed In: ['crossref']
Access and Citation
Cited By Count: 4
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot