Towards a Theory of Regular MSC Languages
Jesper G. Henriksen
December 1999 |
Abstract:
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 Available as PostScript, PDF, DVI. |