Towards a Theory of Regular MSC Languages

Abstract

Message Sequence Charts (MSCs) are an attractive visual formalism<br /> widely used to capture system requirements during the early<br />design stages in domains such as telecommunication software. It is<br />fruitful to have mechanisms for specifying and reasoning about <br />collections of MSCs so that errors can be detected even at the requirements<br /> level. We propose, accordingly, a notion of regularity for <br />collections of MSCs and explore its basic properties. In particular, we<br />provide an automata-theoretic characterization of regular MSC <br />languages in terms of finite-state distributed automata called bounded<br />message-passing automata. These automata consist of a set of <br />sequential processes that communicate with each other by sending and<br />receiving messages over bounded FIFO channels. We also provide a<br />logical characterization in terms of a natural monadic second-order<br />logic interpreted over MSCs.<br />A commonly used technique to generate a collection of MSCs is<br />to use a Message Sequence Graph (MSG). We show that the class of<br />languages arising from the so-called locally synchronized MSGs constitute<br /> a proper subclass of the languages which are regular in our sense.<br />In fact, we characterize the locally synchronized MSG languages as<br />the subclass of regular MSC languages that are finitely generated.