Abstract / Description of output
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
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 language | English |
|---|---|
| Title of host publication | Proceedings of the 22nd International Conference on on Software Engineering, ICSE 2000, Limerick Ireland, June 4-11, 2000. |
| Pages | 304-313 |
| Number of pages | 10 |
| ISBN (Electronic) | 1-58113-206-9 |
| DOIs | |
| Publication status | Published - 2000 |