Modelling, specifying, and verifying message passing systems

We present a model for Message Passing Systems unifying concepts of message sequence charts (MSCs) and Lamport diagrams. Message passing systems may be defined-similarly to MSCs-without having a concrete communication medium in mind. Our main contribution is that we equip such systems with a tool set of specification and verification procedures. We provide a global linear time temporal logic which may be employed for specifying message passing systems. In an independent step, a communication channel may be specified. Given both specifications, we construct a Buchi automaton accepting those linearisations of MSCs which satisfy the given formula and correspond to a fixed but arbitrary channel.