Inference of message sequence charts

  • Alur R
  • Etessami K
  • Yannakakis M
  • 39


    Mendeley users who have this article in their library.
  • 105


    Citations of this article.


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 we 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 then provide polynomial-time algorithms for implication, realizability, and synthesis.

Author-supplied keywords

  • Concurrent state machines
  • Deadlock freedom
  • Formal verification
  • Message sequence charts
  • Realizability
  • Requirements analysis
  • Scenarios
  • Synthesis

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • Rajeev Alur

  • Kousha Etessami

  • Mihalis Yannakakis

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free