This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
From Live Sequence Charts to State Machines and Back: A Guided Tour
December 2005 (vol. 31 no. 12)
pp. 999-1014
The problem of relating state-based intraagent (or intraobject) behavioral descriptions with scenario-based interagent (interobject) descriptions has recently focused much interest among the software engineering community. This paper compiles the results of our investigation of this problem. As interagent formalism, we adopt a simple variant of Live Sequence Charts. For the intraagent perspective, we consider a game-theoretic foundation, looking at agents as "strategies,” which encompasses the popular "state-based” paradigm. Three classes of relationships between models are studied: scenario checking (called eLSC checking), synthesis, and verification. We set a formally defined theoretical stage that allows us to express these three problems very simply, to discuss their complexity, and to describe optimal solutions. Our study reveals the intrinsic high computational difficulty of these tasks. Consequently, many related problems and solutions are surveyed, some of which can be the basis for practical solutions. In this, we also offer a panorama of current research and directions for the future.

[1] D. Harel, “From Play-In Scenarios to Code: An Achievable Dream,” Computer, vol. 34, no. 1, pp. 53-60, Jan. 2001.
[2] L. Lamport and N. Lynch, Handbook of Theoretical Computer Science, vol. B, chapter 18, “Distributed Computing: Models and Methods,” pp. 1157-1199. Amsterdam and Cambridge, Mass.: Elsevier-MIT Press, 1990.
[3] D. Harel and A. Pnueli, “On the Development of Reactive Systems,” NATO ASI Series, K. Apt, ed., vol. F-13, pp. 477-498. New York: Springer, Jan. 1985
[4] J. Mukerji and J. Miller, “MDA Guide v 1. 0. 1 (OMG),” Mar. 2003, http://www. omg. org/mda.
[5] K. Weidenhaupt, K. Pohl, M. Jarke, and P. Haumer, “Scenario Usage in System Development: A Report on Current Practice,” IEEE Software, vol. 15, no. 2, pp. 34-45, Mar./Apr. 1998.
[6] W. Damm and D. Harel, “LSCs: Breathing Life into Message Sequence Charts,” Formal Methods in System Design, vol. 19, no. 1, pp. 45-80, 2001.
[7] D. Harel and R. Marelly, Come, Let's Play! Scenario-Based Programming Using LSCs and the Play-Engine. Springer, 2003.
[8] “MSC-2004: ITU-T Recommendation Z.120: Message Sequence Chart (MSC),” Int'l Telecomm. Union (prev. CCITT), 2004. Draft version, still unapproved.
[9] OMG UML Specification (2.0), Object Management Group (UML Revision Task Force), Sept. 2003, http://www. omg. orguml.
[10] Y. Bontemps, “Relating Inter-Agent and Intra-Agent Specifications (the Case of Live Sequence Charts),” PhD dissertation, Facultés Universitaires Notre-Dame de la Paix, Institut d'Informatique (Univ. of Namur, Computer Science Dept.), Apr. 2005.
[11] M.V. e Cengarle and A. Knapp, “UML 2. 0 Interactions: Semantics and Refinement,” Proc. Third Int'l Workshop Critical Systems Development with UML (CSDUML '04), J. Jürjens, E.B. Fernandez, R. France, and B. Rumpe, eds., pp. 85-99, 2004.
[12] Y. Bontemps, “On the Semantics of UML 2.0 Interaction Diagram,” technical report, Univ. of Namur, Institut d'Informatique, 2004.
[13] M. Jackson, , Software Requirements and Specifications: A Lexicon of Practice, Principles and Prejudices. Addison Wesley, 1995.
[14] N.A. Lynch and M.R. Tuttle, “An Introduction to Input/Output Automata,” CWI Quarterly, vol. 2, no. 3, pp. 219-246, 1989.
[15] Y. Bontemps, P.-Y. Schobbens, and C. Löding, “Synthesis of Open Reactive Systems from Scenario-Based Specifications,” Fundamenta Informaticae, vol. 62, no. 2, pp. 139-169, July 2004.
[16] C. Gunter, A.E. Gunter, L.M. Jackson, and P. Zave, “A Reference Model for Requirements and Specification,” IEEE Software, vol. 17, no. 3, pp. 37-43, May/June 2000.
[17] M. Abadi, L. Lamport, and P. Wolper, “Realizable and Unrealizable Specifications of Reactive Systems,” Automata, Languages, and Programming, Proc. 16th Int'l Colloquium (ICALP '89), G. Ausiello, M. Dezani-Ciancaglini, and S.R.D. Rocca, eds., July 1989.
[18] A. Pnueli, and R. Rosner, “On the Synthesis of a Reactive Module,” Proc. 16th Ann. ACM Symp. Principles of Programming Languages, pp. 179-190, 1989.
[19] G. Berry, “The Foundations of Esterel,” Proof, Language, and Interaction: Essays in Honour of Robin Milner, G. Plotkin, C. Stirling, and M. Tofte, eds. MIT Press, 1998, ftp://ftp-sop.inria.fr/meije/esterel/papers foundations.pdf.
[20] H. Kugler, D. Harel, A. Pnueli, L. Yuan, and Y. Bontemps, “Temporal Logic for Live Sequence Charts,” Proc. Tools and Algorithms for Construction and Analysis of Systems (TACAS '05), Apr. 2005.
[21] Y. Bontemps and P.-Y. Schobbens, “The Complexity of Live Sequence Charts,” Proc. Foundations of Software Science and Computation Structure (FoSSACS '05), V. Sassone, ed., pp. 364-378, Apr. 2005.
[22] D. Harel, H. Kugler, R. Marelly, and A. Pnueli, “Smart Play-Out of Behavioral Requirements,” Proc. Fourth Int'l Conf. Formal Methods in Computer-Aided Design (FMCAD '02), 2002. Also available as Technical Report MCS02-08, The Weizmann Inst. of Science.
[23] Y. Bontemps and P. Heymans, “Turning High-Level Live Sequence Charts into Automata,” Proc. Scenarios and State-Machines: Models, Algorithms, and Tools (SCESM) Workshop, 24th Int'l Conf. Software Eng. (ICSE 2002), May 2002, http://www.cs .tut.fi/tsysta/ICSEpapers/.
[24] D. Harel and H. Kugler, “Synthesizing State-Based Object Systems from LSC Specifications,” Int'l J. Foundations of Computer Science, vol. 13, no. 1, pp. 5-51, Feb. 2002. Preliminary version Proc. Fifth Int'l Conf. Implementation and Application of Automata (CIAA 2000), July 2000.
[25] Automata Logics, and Infinite Games: A Guide to Current Research, E. Grdel, W. Thomas, and T. Wilke, eds. Springer, Nov. 2002, http://link.springer.de/link/service/series/ 0558/tocst2500.htm#toc2500.
[26] D. Harel and M. Politi, Modeling Reactive Systems with Statecharts: The STATEMATE Approach. McGraw-Hill, 1998
[27] P. Wolper and P. Godefroid, “Partial-Order Methods for Temporal Verification,” Proc. Int'l Conf. Concurrency Theory (CONCUR '93), pp. 233-246, 1993.
[28] K. McMillan, Symbolic Model Checking. Kluwer Academic, 1993
[29] N. Wallmeier, P. Hütten, and W. Thomas, “Symbolic Synthesis of Finite-State Controllers for Request-Response Specifications,” Proc. Eighth Int'l Conf. Implementation and Application of Automata (CIAA 2003), O.H. Ibarra, and Z. Dang eds., pp. 11-22, 2003.
[30] R. Rosner, “Modular Synthesis of Reactive Systems,” PhD dissertation, The Weizmann Inst. Science, Rehovot, Israel, Apr. 1992.
[31] A. Pnueli, and R. Rosner, “On the Synthesis of an Asynchronous Reactive Module,” Automata, Languages, and Programming, Proc. 16th Int'l Colloquium (ICALP), G. Ausiello, M. Dezani-Ciancaglini, and S.R.D. Rocca eds., pp. 652-671, July 1989.
[32] O. Kupferman, and M.Y. Vardi, “Synthesizing Distributed Systems,” Proc. 16th IEEE Symp. Logic in Computer Science, July 2001.
[33] P. Gastin, B. Lerman, and M. Zeitoun, “Distributed Games and Distributed Control for Asynchronous Systems,” Proc. Latin Am. Theoretical Informatics (LATIN '04), Apr. 2004, http://www.liafa. jussieu.fr/~versydis/data/ publicationsGastinLermanZeitoun-LATIN04.pdf .
[34] P. Madhusudhan and P. Thiagarajan, “A Decidable Class of Asynchronous Distributed Controllers,” Proc. CONCUR '02, 2002, http://www.cis.upenn.edu/madhusudconcur02.ps.gz .
[35] D. Harel, H. Kugler, and A. Pnueli, “Synthesis Revisited: Generating Statechart Models from Scenario-Based Requirements,” Formal Methods in Software and Systems Modeling, H.-J. Kreowski, U. Montanari, F. Orejas, G. Rozenberg, and G. Taentzer, eds., pp. 309-324, 2005.
[36] Y. Bontemps and P. Heymans, “As Fast as Sound (Lightweight Formal Scenario Synthesis and Verification),” Proc. Third Int'l Workshop Scenarios and State Machines: Models, Algorithms, and Tools (SCESM '04), H. Giese, and I. Krüger, eds., pp. 27-34, May 2004. http://www.info.fundp.ac.be~ybo.
[37] Y. Bontemps, P. Heymans, and P.-Y. Schobbens, “Lightweight Formal Methods for Scenario-Based Software Engineering,” Scenarios, T. Systä, and S. Leue, eds., pp. 174-192. Springer, 2005.
[38] J. Sun, and J.S. Dong, “Synthesis of Distributed Processes from Scenario-Based Specifications,” Formal Methods (FM 2005), 2005.
[39] T. Homme and J.E. Ramsland, “From Live Sequence Charts to Implementation (a Study of the LSC Specification, the Execution of Behavioral Requirements and Exploring the Possibilities to Use an LSC Model to Generate Java Code),” master's thesis, Agder Univ. College, Agder, Norway, 2003.
[40] O. Kupferman and M.Y. Vardi, “Synthesis with Incomplete Information,” Proc. Second Int'l Conf. Temporal Logic, pp. 91-106, July 1997.
[41] M.Y. Vardi, “An Automata-Theoretic Approach to Fair Realizability and Synthesis,” Proc. Seventh Int'l Conf. Computer Aided Verification, P. Wolper, ed., pp. 267-278. Springer Verlag, 1995, http://citeseer.nj.nec.com/articlevardi95automatatheoretic .html .
[42] P.J.G. Ramadge, and W.M. Wonham, “The Control of Discrete Event Systems,” Proc. IEEE, special issue on dynamics of discrete event systems, vol. 77, no. 1, pp. 81-98, 1989.
[43] H. Wong-Toi and D.L. Dill, “Synthesizing Processes and Schedulers from Temporal Specifications,” Computer-Aided Verification '90: Proc. DIMACS Workshop, E.M. Clarke and R.P. Kurshan, eds., pp. 177-186, 1991.
[44] Z. Manna and P. Wolper, “Synthesis of Communicating Processes from Temporal Logic Specifications,” ACM Trans. Programming Languages and Systems (TOPLAS), vol. 6, no. 1, pp. 68-93, 1984.
[45] E.A. Emerson and E.M. Clarke, “Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons,” Science of Computer Programming, vol. 2, no. 3, pp. 241-266, Dec. 1982.
[46] D. Amyot and A. Eberlein, “An Evaluation of Scenario Notations for Telecommunication Systems Development,” Proc. Ninth Int'l Conf. Telecomm. Systems (9ICTS), Mar. 2001.
[47] K. Koskimies, T. Männistö, T. Systä, and J. Tuomi, “SCED: A Tool for Dynamic Modelling of Object Systems,” Technical Report A-1996-4, Dept. of Computer Science, Univ. of Tampere, Finland, July 1996.
[48] A.W. Biermann and R. Krishnaswamy, “Constructing Programs from Example Computations,” IEEE Trans. Software Eng. (TSE), vol. 2, no. 3, pp. 141-153, Sept. 1976.
[49] I. Diethelm, L. Geiger, T. Maier, and A. Zündorf, “Turning Collaboration Diagram Strips into Storycharts,” Proc. Scenarios and State-Machines: Models, Algorithms, and Tools (SCESM) Workshop 24th Int'l Conf. Software Eng. (ICSE 2002), May 2002, http://www.cs.tut.fi/~tsysta/ICSEpapers/.
[50] E. Mäkinen and T. Systä, “Minimally Adequate Teacher Synthesizes Statechart Diagrams,” Acta Informatica, vol. 38, pp. 235-259, 2002.
[51] J. Koskinen, E. Mäkinen, and T. Systä, “Minimally Adequate Teacher Synthesizes Shuttles, Too,” Proc. Third Int'l Workshop Scenarios and State Machines: Models, Algorithms, and Tools (SCESM '04), H. Giese, and I. Krüger, eds., May 2004.
[52] P. Hsia, J. Samuel, J. Gao, D. Kund, Y. Toyoshima, and C. Chen, “Formal Approach to Scenario Analysis,” IEEE J., pp. 33-41, Mar. 1994.
[53] I. Krüger, R. Grosu, P. Scholz, and M. Broy, From MSCs to Statecharts, F.J. Rammig, ed. Kluwer Academic, 1999.
[54] J. Whittle, and J. Schumann, “Generating Statechart Designs from Scenarios,” Proc. 22nd Int'l Conf. Software Eng. (ICSE 2000), pp. 314-323, June 2000.
[55] S. Uchitel and J. Kramer, “A Workbench for Synthesizing Behaviour Models from Scenarios,” Proc. 23rd IEEE Int'l Conf. Software Eng. (ICSE '01), 2001.
[56] R. Alur, K. Etessami, and M. Yannakakis, “Inference of Message Sequence Charts,” Proc. 22nd Int'l Conf. Software Eng., pp. 304-313, 2000.
[57] T. Ziadi, L. Hélouët, and J.-M. Jézéquel, “Revisiting Statechart Synthesis with an Algebraic Approach,” Proc. 26th Int'l Conf. Software Eng. (ICSE), pp. 242-251, May 2004.
[58] S. Uchitel, J. Kramer, and J. Magee, “Detecting Implied Scenarios in Message Sequence Chart Specifications,” Proc. Joint Eighth European Software Eng. Conf. and Ninth ACM SIGSOFT Symp. Foundation of Software Eng. (ESEC/FSE-01), V. Gruhn, ed., pp. 74-82, Sept. 2001.
[59] B. Finkbeiner, and I.H. Krüger, “Using Message Sequence Charts for Component-Based Formal Verification,” Proc. OOPSLA 2001 Workshop Specification and Verification of Component-Based Systems, Oct. 2001.
[60] J. Desharnais, M. Frappier, R. Khédri, and A. Mili, “Integration of Sequential Scenarios,” IEEE Trans. Software Eng., vol. 24, no. 9, pp. 695-708, Sept. 1998.
[61] K.E. Wiegers, Software Requirements, second ed. Microsoft Press, Feb. 2003.
[62] M. Vardi and P. Wolper, “Automata-Theoretic Techniques for Modal Logics of Programs,” J. Computer and System Science, vol. 32, no. 2, pp. 183-221, Apr. 1986.
[63] S. Schwoon and J. Esparza, “A Note on On-the-Fly Verification Algorithms,” Tools and Algorithms for Analysis and Construction of Systems (TACAS 2005), N. Halbwachs, and L.D. Zuck, eds., pp. 174-190, 2005.
[64] J. Klose, and H. Wittke, “An Automata Based Interpretation of Live Sequence Charts,” Proc. TACAS (Tools and Algorithms for the Construction and Analysis of Systems), T. Margaria, and W. Yi, eds., pp. 512, Apr. 2001.
[65] J. Klose, T. Kropf, and J. Ruf, “A Visual Approach to Validating System Level Designs,” ISSS '02: Proc. 15th Int'l Symp. System Synthesis, pp. 186-191, 2002.
[66] J. Bohn, W. Damm, J. Klose, A. Moik, and H. Wittke, “Modeling and Validating Train System Applications Using Statemate and Live Sequence Charts,” Proc. Conf. Integrated Design and Process Technology (IDPT 2002), H. Ehrig, B.J. Krämer, and A. Ertas, eds., 2002, http://ca.informatik.uni-oldenburg.de/cgi-bin bibsearch ?author=Wittke.
[67] J. Klose, “Live Sequence Charts: A Graphical Formalism for the Specification of Communication Behavior,” PhD dissertation, Carl von Ossietzky Universität, Oldenburg, 2003.
[68] M. Brill, R. Buschermöhle, W. Damm, J. Klose, B. Westphal, and H. Wittke, “Formal Verification of LSCs in the Verification Process,” Integration of Software Specification Techniques for Applications in Eng., M. Grosse-Rhode, W. Reif, E. Schnieder, and E. Westkämper, eds., 2004.
[69] O. Kupferman, M.Y. Vardi, and P. Wolper, “Module Checking,” Information and Computation, vol. 164, pp. 322-344, 2001.
[70] E.M. Clarke and J.M. Wing, “Formal Methods: State of the Art and Future Directions,” ACM Computing Surveys, vol. 28, no. 4, pp. 626-643, Dec. 1996.
[71] A. Bunker and G. Gopalakrishnan, “Verifying a Virtual Component Interface-Based PCI Bus Wrapper Using an LSC-Based Specification,” Technical Report UUCS-02-004, School of Computing, Univ. of Utah, 2002.
[72] Y. Bontemps, “Automated Verification of State-Based Specifications against Scenarios (A Step towards Relating Inter-Object to Intra-Object Specifications),” master's thesis, Univ. of Namur, Namur, Belgium, June 2001.

Index Terms:
Index Terms- Requirements engineering, life cycle, program verification.
Citation:
Yves Bontemps, Patrick Heymans, Pierre-Yves Schobbens, "From Live Sequence Charts to State Machines and Back: A Guided Tour," IEEE Transactions on Software Engineering, vol. 31, no. 12, pp. 999-1014, Dec. 2005, doi:10.1109/TSE.2005.137
Usage of this product signifies your acceptance of the Terms of Use.