Semantics of nondeterministic asynchronous broadcast networks (Q2366562)

The authors develop a language for asynchronous broadcast communication based on variants of CSP (Communicating Sequential Processes). The language is used to model and analyze the various categories of broadcast communications such as Ethernet. The paper is a first attempt at a classification and a formal treatment of broadcast using a realistic real-time model. The authors give a syntax-directed compositional denotational semantics for a spectrum of nondeterministic broadcast networks of processes under the maximal parallelism model applying a simple semantics domain of prefix-closed state-history pairs. The semantics provides a model of various broadcast categories. This model leads to a specification-oriented semantics of broadcast networks, forming a basis for a compositional verification of such systems.