Inference of message sequence charts

Rajeev Alur, Kousha Etessami, Mihalis Yannakakis

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Soft we are 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 SCs? If on the other hand other unspecified and possibly unwanted scenarios are "implied" by their MSCs can the softw are 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
Original languageEnglish
Title of host publicationProceedings of the 22nd International Conference on on Software Engineering, ICSE 2000, Limerick Ireland, June 4-11, 2000.
Pages304-313
Number of pages10
ISBN (Electronic)1-58113-206-9
DOIs
Publication statusPublished - 2000

Fingerprint

Dive into the research topics of 'Inference of message sequence charts'. Together they form a unique fingerprint.

Cite this