We present a model for Message Passing Systems unifying concepts of message sequence charts (MSCs) and Lam-port 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 linearizations of MSCs which satisfy the given formula and correspond to a fixed but arbitrary channel.
展开▼
