
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Yves Bontemps, Patrick Heymans, PierreYves Schobbens, "From Live Sequence Charts to State Machines and Back: A Guided Tour," IEEE Transactions on Software Engineering, vol. 31, no. 12, pp. 9991014, December, 2005.  
BibTex  x  
@article{ 10.1109/TSE.2005.137, author = {Yves Bontemps and Patrick Heymans and PierreYves Schobbens}, title = {From Live Sequence Charts to State Machines and Back: A Guided Tour}, journal ={IEEE Transactions on Software Engineering}, volume = {31}, number = {12}, issn = {00985589}, year = {2005}, pages = {9991014}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2005.137}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  From Live Sequence Charts to State Machines and Back: A Guided Tour IS  12 SN  00985589 SP999 EP1014 EPD  9991014 A1  Yves Bontemps, A1  Patrick Heymans, A1  PierreYves Schobbens, PY  2005 KW  Index Terms Requirements engineering KW  life cycle KW  program verification. VL  31 JA  IEEE Transactions on Software Engineering ER   
[1] D. Harel, “From PlayIn Scenarios to Code: An Achievable Dream,” Computer, vol. 34, no. 1, pp. 5360, Jan. 2001.
[2] L. Lamport and N. Lynch, Handbook of Theoretical Computer Science, vol. B, chapter 18, “Distributed Computing: Models and Methods,” pp. 11571199. Amsterdam and Cambridge, Mass.: ElsevierMIT Press, 1990.
[3] D. Harel and A. Pnueli, “On the Development of Reactive Systems,” NATO ASI Series, K. Apt, ed., vol. F13, pp. 477498. 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. 3445, 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. 4580, 2001.
[7] D. Harel and R. Marelly, Come, Let's Play! ScenarioBased Programming Using LSCs and the PlayEngine. Springer, 2003.
[8] “MSC2004: ITUT 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 InterAgent and IntraAgent Specifications (the Case of Live Sequence Charts),” PhD dissertation, Facultés Universitaires NotreDame 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. 8599, 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. 219246, 1989.
[15] Y. Bontemps, P.Y. Schobbens, and C. Löding, “Synthesis of Open Reactive Systems from ScenarioBased Specifications,” Fundamenta Informaticae, vol. 62, no. 2, pp. 139169, 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. 3743, 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. DezaniCiancaglini, 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. 179190, 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://ftpsop.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. 364378, Apr. 2005.
[22] D. Harel, H. Kugler, R. Marelly, and A. Pnueli, “Smart PlayOut of Behavioral Requirements,” Proc. Fourth Int'l Conf. Formal Methods in ComputerAided Design (FMCAD '02), 2002. Also available as Technical Report MCS0208, The Weizmann Inst. of Science.
[23] Y. Bontemps and P. Heymans, “Turning HighLevel Live Sequence Charts into Automata,” Proc. Scenarios and StateMachines: 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 StateBased Object Systems from LSC Specifications,” Int'l J. Foundations of Computer Science, vol. 13, no. 1, pp. 551, 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. McGrawHill, 1998
[27] P. Wolper and P. Godefroid, “PartialOrder Methods for Temporal Verification,” Proc. Int'l Conf. Concurrency Theory (CONCUR '93), pp. 233246, 1993.
[28] K. McMillan, Symbolic Model Checking. Kluwer Academic, 1993
[29] N. Wallmeier, P. Hütten, and W. Thomas, “Symbolic Synthesis of FiniteState Controllers for RequestResponse Specifications,” Proc. Eighth Int'l Conf. Implementation and Application of Automata (CIAA 2003), O.H. Ibarra, and Z. Dang eds., pp. 1122, 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. DezaniCiancaglini, and S.R.D. Rocca eds., pp. 652671, 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/ publicationsGastinLermanZeitounLATIN04.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 ScenarioBased Requirements,” Formal Methods in Software and Systems Modeling, H.J. Kreowski, U. Montanari, F. Orejas, G. Rozenberg, and G. Taentzer, eds., pp. 309324, 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. 2734, May 2004. http://www.info.fundp.ac.be~ybo.
[37] Y. Bontemps, P. Heymans, and P.Y. Schobbens, “Lightweight Formal Methods for ScenarioBased Software Engineering,” Scenarios, T. Systä, and S. Leue, eds., pp. 174192. Springer, 2005.
[38] J. Sun, and J.S. Dong, “Synthesis of Distributed Processes from ScenarioBased 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. 91106, July 1997.
[41] M.Y. Vardi, “An AutomataTheoretic Approach to Fair Realizability and Synthesis,” Proc. Seventh Int'l Conf. Computer Aided Verification, P. Wolper, ed., pp. 267278. 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. 8198, 1989.
[43] H. WongToi and D.L. Dill, “Synthesizing Processes and Schedulers from Temporal Specifications,” ComputerAided Verification '90: Proc. DIMACS Workshop, E.M. Clarke and R.P. Kurshan, eds., pp. 177186, 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. 6893, 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. 241266, 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 A19964, 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. 141153, Sept. 1976.
[49] I. Diethelm, L. Geiger, T. Maier, and A. Zündorf, “Turning Collaboration Diagram Strips into Storycharts,” Proc. Scenarios and StateMachines: 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. 235259, 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. 3341, 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. 314323, 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. 304313, 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. 242251, 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/FSE01), V. Gruhn, ed., pp. 7482, Sept. 2001.
[59] B. Finkbeiner, and I.H. Krüger, “Using Message Sequence Charts for ComponentBased Formal Verification,” Proc. OOPSLA 2001 Workshop Specification and Verification of ComponentBased 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. 695708, Sept. 1998.
[61] K.E. Wiegers, Software Requirements, second ed. Microsoft Press, Feb. 2003.
[62] M. Vardi and P. Wolper, “AutomataTheoretic Techniques for Modal Logics of Programs,” J. Computer and System Science, vol. 32, no. 2, pp. 183221, Apr. 1986.
[63] S. Schwoon and J. Esparza, “A Note on OntheFly Verification Algorithms,” Tools and Algorithms for Analysis and Construction of Systems (TACAS 2005), N. Halbwachs, and L.D. Zuck, eds., pp. 174190, 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. 186191, 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.unioldenburg.de/cgibin 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. GrosseRhode, 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. 322344, 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. 626643, Dec. 1996.
[71] A. Bunker and G. Gopalakrishnan, “Verifying a Virtual Component InterfaceBased PCI Bus Wrapper Using an LSCBased Specification,” Technical Report UUCS02004, School of Computing, Univ. of Utah, 2002.
[72] Y. Bontemps, “Automated Verification of StateBased Specifications against Scenarios (A Step towards Relating InterObject to IntraObject Specifications),” master's thesis, Univ. of Namur, Namur, Belgium, June 2001.