## Inference of Message Sequence Charts

*Rajeev Alur, Kousha Etessami, and Mihalis Yannakakis*
Software designers draw
Message Sequence Charts for
early modeling of the individual behaviors they
expect from the concurrent system under design. Can they be sure
that precisely the behaviors they have
described are realizable by some implementation
of the components of the concurrent system?
If so, can one automatically synthesize concurrent state machines
realizing the given MSCs?
If, on the other hand, other unspecified and possibly unwanted
scenarios are ``implied'' by their
MSCs, can the software designer be automatically warned
and provided the implied MSCs?

In this paper we provide a framework in which all these questions are
answered positively. We first describe the formal framework within
which one can derive implied MSCs , and we then
provide polynomial-time algorithms for implication, realizability, and synthesis. In
particular, we describe a novel algorithm for checking deadlock-free
(safe) realizability.

To appear in the
*Proceedings of the
22nd International Conference on Software Engineering*
(ICSE'00), pp. 304--313, 2000.