This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Inference of Message Sequence Charts
July 2003 (vol. 29 no. 7)
pp. 623-633

Abstract—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.

[1] ITU-T Recommendation Z. 120. Message Sequence Charts (MSC '96) ITU Telecommunication Standardization Sector, May 1996.
[2] E. Rudolph, P. Graubmann, and J. Gabowski, Tutorial on Message Sequence Charts Computer Networks and ISDN Systems SDL and MSC, vol. 28, 1996.
[3] J. Rumbaugh, I. Jacobson, and G. Booch, The Unified Modeling Language Reference Manual. Addison-Wesley, 1999.
[4] R. Alur, G.J. Holzmann, and D. Peled, An Analyzer for Message Sequence Charts Software Concepts and Tools, vol. 17, no. 2, pp. 70-77, 1996.
[5] A. Muscholl, D. Peled, and Z. Su, Deciding Properties of Message Sequence Charts Foundations of Software Science and Computer Structures, 1998.
[6] H. Ben-Abdallah and S. Leue, Syntactic Detection of Process Divergence and Nonlocal Choice in Message Sequence Charts Proc. Second Int'l Workshop Tools and Algorithms for the Construction and Analysis of Systems, 1997.
[7] R. Alur and M. Yannakakis, Model Checking of Message Sequence Charts Proc. CONCUR'99: Concurrency Theory, 10th Int'l Conf., pp. 114-129, 1999.
[8] G.J. Holzmann, D.A. Peled, and M.H. Redberg, Design Tools for Requirements Engineering Bell Labs Technical J., vol. 2, no. 1, pp. 86-95, 1997.
[9] H. Ben-Abdallah and S. Leue, MESA: Support for Scenario-Based Design of Concurrent Systems Proc. Fourth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 118-135, 1998.
[10] K. Koskimies, T. Männistö, T. Systä, and J. Tuomi, Automated Support for OO Software IEEE Software, vol. 15, no. 1, pp. 87-94, Jan./Feb. 1998.
[11] I. Kruger, R. Grosu, P. Scholz, and M. Broy, From MSCs to Statecharts Distributed and Parallel Embedded Systems, 1999.
[12] S. Leue, L. Mehrmann, and M. Rezai, Synthesizing ROOM Models from Message Sequence Chart Specifications Proc. 13th IEEE Conf. Automated Software Eng., 1998.
[13] G.J. Holzmann, Early Fault Detection Tools Proc. Sixth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '96), 1996.
[14] K. Koskimies and E. Makinen, Automatic Synthesis of State Machines from Trace Diagrams Software-Practice and Experience, vol. 24, no. 7, pp. 643-658, 1994.
[15] D. Harel and H. Kugler, Synthesizing Object Systems from LSC Specifications unpublished draft, 1999.
[16] W. Damm and D. Harel, LSCs: Breathing Life into Message Sequence Charts Proc. Third IFIP Conf. Formal Methods for Open Object-Based Distributed Systems (FMOODS '99), pp. 293-312, 1999.
[17] M. Mukund, K.N. Kumar, and M. Sohoni, Synthesizing Distributed Finite-State Systems from MSCs Proc. CONCUR 2000: Concurrency Theory, 11th Int'l Conf., 2000.
[18] A.W. Biermann and J.A. Feldman, On the Synthesis of Finite State Machines from Samples of Their Behavior IEEE Trans. Computers, pp. 592-597, 1972.
[19] D. Angluin and C.H. Smith, Inductive Inference: Theory and Methods ACM Computing Surveys, vol. 15, pp. 237-269, 1983.
[20] C. Papadimitriou, The Theory of Database Concurrency Control. Computer Science Press, 1986.
[21] The Book of Traces. V. Diekert and G. Rozenberg, eds., World Scientific Publishing, 1995.
[22] M. Lohrey, Safe Realizability of High-Level Message Sequence Charts Proc. CONCUR 2002: Concurrency Theory, 13th Int'l Conf., 2002.
[23] D. Maier, Y. Sagiv, and M. Yannakakis, On the Complexity of Testing Implications of Functional and Join Dependencies J. ACM, vol. 28, no. 4, pp. 680-695, 1981.
[24] R. Alur, K. Etessami, and M. Yannakakis, Inference of Message Sequence Charts Proc. 22nd Int'l Conf. Software Eng., pp. 304-313, 2000.
[25] R. Alur, K. Etessami, and M. Yannakakis, Inference of Message Sequence Charts technical report, Laboratory for Foundations of Computer Science, Univ. of Edinburgh, 2003, http://homepages. inf.ed.ac.uk/koushamsc_inference_j_v.ps .

Index Terms:
Message sequence charts, requirements analysis, formal verification, scenarios, concurrent state machines, deadlock freedom, realizability, synthesis.
Citation:
Rajeev Alur, Kousha Etessami, Mihalis Yannakakis, "Inference of Message Sequence Charts," IEEE Transactions on Software Engineering, vol. 29, no. 7, pp. 623-633, July 2003, doi:10.1109/TSE.2003.1214326
Usage of this product signifies your acceptance of the Terms of Use.