|
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
Hierarchical Message Sequence Chart (HMSC). We show that the class of
languages arising from the so-called bounded HMSCs constitute a proper
subclass of the class of regular MSC languages. In fact, we characterize the
bounded HMSC languages as the subclass of regular MSC languages that are
finitely generated.
[.pdf]
|