
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Rajeev Alur, Kousha Etessami, Mihalis Yannakakis, "Inference of Message Sequence Charts," IEEE Transactions on Software Engineering, vol. 29, no. 7, pp. 623633, July, 2003.  
BibTex  x  
@article{ 10.1109/TSE.2003.1214326, author = {Rajeev Alur and Kousha Etessami and Mihalis Yannakakis}, title = {Inference of Message Sequence Charts}, journal ={IEEE Transactions on Software Engineering}, volume = {29}, number = {7}, issn = {00985589}, year = {2003}, pages = {623633}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2003.1214326}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Inference of Message Sequence Charts IS  7 SN  00985589 SP623 EP633 EPD  623633 A1  Rajeev Alur, A1  Kousha Etessami, A1  Mihalis Yannakakis, PY  2003 KW  Message sequence charts KW  requirements analysis KW  formal verification KW  scenarios KW  concurrent state machines KW  deadlock freedom KW  realizability KW  synthesis. VL  29 JA  IEEE Transactions on Software Engineering ER   
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 polynomialtime algorithms for implication, realizability, and synthesis.
[1] ITUT 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. AddisonWesley, 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. 7077, 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. BenAbdallah 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. 114129, 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. 8695, 1997.
[9] H. BenAbdallah and S. Leue, MESA: Support for ScenarioBased Design of Concurrent Systems Proc. Fourth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 118135, 1998.
[10] K. Koskimies, T. Männistö, T. Systä, and J. Tuomi, Automated Support for OO Software IEEE Software, vol. 15, no. 1, pp. 8794, 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 SoftwarePractice and Experience, vol. 24, no. 7, pp. 643658, 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 ObjectBased Distributed Systems (FMOODS '99), pp. 293312, 1999.
[17] M. Mukund, K.N. Kumar, and M. Sohoni, Synthesizing Distributed FiniteState 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. 592597, 1972.
[19] D. Angluin and C.H. Smith, Inductive Inference: Theory and Methods ACM Computing Surveys, vol. 15, pp. 237269, 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 HighLevel 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. 680695, 1981.
[24] R. Alur, K. Etessami, and M. Yannakakis, Inference of Message Sequence Charts Proc. 22nd Int'l Conf. Software Eng., pp. 304313, 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 .