Abstract
Constructing a program from a specification is a long-known general and fundamental problem. Besides its theoretical interest, this question also has practical implications, since finding good synthesis algorithms could bring about a major improvement in the reliable development of complex systems. In this paper we describe a methodology for synthesizing statechart models from scenario-based requirements. The requirements are given in the language of live sequence charts (LSCs), and may be played in directly from the GUI, and the resulting statecharts are of the object-oriented variant, as adopted in the UML. We have implemented our algorithms as part of the Play-Engine tool and the generated statechart model can then be executed using existing UML case tools.
This research was supported in part by the John von Neumann Minerva Center for the Verification of Reactive Systems, by the European Commission project OMEGA (IST-2001-33522) and by the Israel Science Foundation (grant No. 287/02-1).
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Synthesis Approach
- Synthesis Algorithm
- Message Sequence Chart
- Behavioral Requirement
- Live Sequence Chart
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Yannakakis, M.: Model checking of message sequence charts. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 114–129. Springer, Heidelberg (1999)
Arons, T., Hooman, J., Kugler, H., Pnueli, A., van der Zwaag, M.: Deductive Verification of UML Models in TLPVS. In: Baar, T., Strohmeier, A., Moreira, A., Mellor, S.J. (eds.) UML 2004. LNCS, vol. 3273, pp. 335–349. Springer, Heidelberg (2004)
Barak, D., Harel, D., Marelly, R.: InterPlay: Horizontal Scale-Up and Transition to Design in Scenario-Based Programming. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 66–86. Springer, Heidelberg (2004)
Biermann, A.W., Krishnaswamy, R.: Constructing programs from example computations. IEEE Trans. Softw. Eng. SE-2, 141–153 (1976)
Bontemps, Y., Schobbens, P.Y.: Synthesizing open reactive systems from scenario-based specifications. In: Proc. of the 3rd Int. Conf. on Application of Concurrency to System Design (ACSD 2003). IEEE Computer Society Press, Los Alamitos (2003)
Buchi, J.R.: State-strategies for games in F σδ ∩G δσ . J. Symb. Logic 48, 1171–1198 (1983)
Damm, W., Harel, D.: LSCs: Breathing life into message sequence charts. Formal Methods in System Design 19(1), 45–80 (2001); Preliminary version appeared in Proc. 3rd IFIP Int. Conf. on Formal Methods for Open Object-Based Distributed Systems (FMOODS 1999)
Emerson, E.A.: Temporal and modal logics. In: van Leeuwen, J. (ed.) Handbook of theoretical computer science, vol. B, pp. 995–1072. Elsevier, Amsterdam (1990)
Fisher, J., Harel, D., Hubbard, E.J.A., Piterman, N., Stern, M.J., Swerdlin, N.: Combining state-based and scenario-based approaches in modeling biological systems. In: Danos, V., Schachter, V. (eds.) CMSB 2004. LNCS (LNBI), vol. 3082, pp. 236–241. Springer, Heidelberg (2005)
Harel, D., Kugler, H.: Synthesizing state-based object systems from LSC specifications. Int. J. of Foundations of Computer Science (IJFCS) 13(1), 5–51 (2002); Yu, S., Păun, A. (eds.): CIAA 2000. LNCS, vol. 2088. Springer, Heidelberg (2001)
Harel, D., Kugler, H., Marelly, R., Pnueli, A.: Smart play-out of behavioral requirements. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 378–398. Springer, Heidelberg (2002); Also available as Tech. Report MCS02-08, The Weizmann Institute of Science
Harel, D., Kugler, H., Weiss, G.: Some Methodological Observations Resulting from Experience Using LSCs and the Play-In/Play-Out Approach. In: Proc. Scenarios: Models, Algorithms and Tools. LNCS. Springer, Heidelberg (2005) (to appear)
Harel, D., Marelly, R.: Come, Let’s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)
Harel, D., Marelly, R.: Specifying and Executing Behavioral Requirements: The Play In/Play-Out Approach. Software and System Modeling (SoSyM) 2(2), 82–107 (2003)
Rhapsody. I-Logix, Inc., products web page, http://www.ilogix.com/products/
Klose, J., Wittke, H.: An automata based interpretation of live sequence chart. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 512. Springer, Heidelberg (2001)
Koskimies, K., Makinen, E.: Automatic synthesis of state machines from trace diagrams. Software – Practice and Experience 24(7), 643–658 (1994)
Koskimies, K., Mannisto, T., Systa, T., Tuomi, J.: SCED: A Tool for Dynamic Modeling of Object Systems. Tech. Report A-1996-4, University of Tampere (July 1996)
Krüger, I., Grosu, R., Scholz, P., Broy, M.: From MSCs to Statecharts. In: Proc. Int. Workshop on Distributed and Parallel Embedded Systems (DIPES 1998), pp. 61–71. Kluwer Academic Publishers, Dordrecht (1999)
Leue, S., Mehrmann, L., Rezai, M.: Synthesizing ROOM models from message sequence chart specifications. Tech. Report 98-06, University of Waterloo (April 1998)
ITU-TS Recommendation Z.120 (11/99): MSC 2000. ITU-TS, Geneva (1999)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. 16th ACM Symp. Princ. of Prog. Lang., pp. 179–190 (1989)
Pnueli, A., Shahar, E.: A platform for combining deductive with algorithmic verification. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 184–195. Springer, Heidelberg (1996)
Rational Rose Technical Developer. Rational, Inc., web page, http://www-306.ibm.com/software/awdtools/developer/technical/
Schinz, I., Toben, T., Westphal, B.: The Rhapsody UML Verification Environment. In: 2nd Int. Conf. on Software Engineering and Formal Methods. IEEE Computer Society Press, Los Alamitos (2004)
Schlor, R., Damm, W.: Specification and verification of system-level hardware designs using timing diagram. In: European Conference on Design Automation, Paris, France, pp. 518–524. IEEE Computer Society Press, Los Alamitos (1993)
Telelogic TAU. Telelogic, Inc., web page, http://www.telelogic.com/products/tau/.
UML. Documentation of the unified modeling language (UML). Available from the Object Management Group (OMG), http://www.omg.org
Whittle, J., Schumann, J.: Generating statechart designs from scenarios. In: 22nd International Conference on Software Engineering (ICSE 2000), pp. 314–323. ACM Press, New York (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Harel, D., Kugler, H., Pnueli, A. (2005). Synthesis Revisited: Generating Statechart Models from Scenario-Based Requirements. In: Kreowski, HJ., Montanari, U., Orejas, F., Rozenberg, G., Taentzer, G. (eds) Formal Methods in Software and Systems Modeling. Lecture Notes in Computer Science, vol 3393. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31847-7_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-31847-7_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-24936-8
Online ISBN: 978-3-540-31847-7
eBook Packages: Computer ScienceComputer Science (R0)