Abstract of Paper

Regular Collections of Message Sequence Charts
by Jesper G. Henriksen, Madhavan Mukund, K. Narayan Kumar, P.S. Thiagarajan


Message Sequence Charts (MSCs) are an attractive visual formalism widely
used to capture system requirements during the early design stages in
domains such as telecommunication software. At this level, the requirements
mainly capture the interaction between the constituent processes in terms of
scenarios described by a collection of MSCs. One popular mechanism for
capturing a collection of scenarios is a Message Sequence Graph (MSG). It is
easy to see, however, that not all MSGs describe collections of MSCs that
can be ``realized'' as a finite-state device. Our main goal is to pin down
this notion of realizability. We do so in a setting which is, to start with,
independent of the notion of MSGs. We propose a notion of \emph{regularity}
for collections of MSCs and explore its basic properties. In particular, we
provide a characterization of regular collections of MSCs in terms of
finite-state distributed automata called bounded message-passing automata. 
These automata consist of a set of sequential processes that communicate
with each other by sending and receiving messages over bounded FIFO
channels. We also provide a logical characterization in terms of a natural
monadic second-order logic interpreted over MSCs. It turns out that
realizable collections of MSCs as specified by MSGs constitute a strict
subclass of the regular collections of MSCs.