2021/05/01 by Erwan Mahe, Mahe, Erwan, Christophe Gaston +3
Computer Science · #Distributed systems and fault tolerance #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Service-Oriented Architecture and Web Services
paper · pdf · doi:10.48550/arxiv.2105.00208
openalex publication_date 2021/05/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Message Sequence Charts & Sequence Diagrams are graphical models that represent the behavior of distributed and concurrent systems via the scheduling of discrete and local emission and reception events. We propose an Interaction Language (IL) to formalize such models, defined as a term algebra which includes strict and weak sequencing, alternative and parallel composition and four kinds of loops. This IL is equipped with a denotational-style 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 both semantics.