Computing Sciences Research
Bell Laboratories
5pm Tuesday 18th June 2002
Room 6206, JCMB, King's Buildings
Message Sequence Charts (MSCs) are a convenient visual notation for describing scenarios of message exchanges in a concurrent system. MSCs have been incorporated in software design notations such as UML; there is an extensive ITU standard associated with them, and there are a number of CASE tools that employ both MSCs and MSC-graphs, which are graphs whose nodes are labeled by MSCs allowing compact specification of a (possibly infinite) set of MSCs.
In this talk, we describe a formal framework for determining whether the executions described by a set of MSCs or an MSC-graph can be realized as precisely the set of executions of communicating state machines. We study algorithms to detect two kinds of realizability: ordinary (weak) as well as safe realizability in which the state machines that realize the MSC set are required to be deadlock-free. We provide a polynomial-time algorithm for safe realizability of MSC sets, whereas we show that weak realizability is coNP-complete. For MSC-graphs, the algorithmic problems become much more complicated. We will show both decidability and undecidability results in this setting.
If a set of MSCs is realizable, then we can synthesize communicating state machines that realize these behaviors. If not, we can infer unspecified but implied MSCs whose behaviors must be exhibited by any realization which includes the specified set. Verification of MSCs and MSC-graphs can then be recast by asking: given MSCs or an MSC-graph, can we efficiently model check the set of all specified as well as implied MSCs, rather than only what was specified? We also address these and related verification questions.
(This talk describes joint work with Rajeev Alur (U. Penn) and Mihalis Yannakakis (Avaya Labs). It is based on the content of two papers that appeared at ICSE'2000 and ICALP'2001.)