Towards a Theory of Regular MSC Languages

Resumé

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. It is
fruitful to have mechanisms for specifying and reasoning about
collections of MSCs so that errors can be detected even at the requirements
level. We propose, accordingly, a notion of regularity for
collections of MSCs and explore its basic properties. In particular, we
provide an automata-theoretic characterization of regular MSC
languages 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.
A commonly used technique to generate a collection of MSCs is
to use a Message Sequence Graph (MSG). We show that the class of
languages arising from the so-called locally synchronized MSGs constitute
a proper subclass of the languages which are regular in our sense.
In fact, we characterize the locally synchronized MSG languages as
the subclass of regular MSC languages that are finitely generated.