Abstract
Live sequence charts (LSCs) have been defined recently as an extension of message sequence charts (MSCs; or their UML variant, sequence diagrams) for rich inter-object specification. One of the main additions is the notion of universal charts and hot, mandatory behavior, which, among other things, enables one to specify forbidden scenarios. LSCs are thus essentially as expressive as statecharts. This paper deals with synthesis, which is the problem of deciding, given an LSC specification, if there exists a satisfying object system and, if so, to synthesize one automatically. The synthesis problem is crucial in the development of complex systems, since sequence diagrams serve as the manifestation of use cases — whether used formally or informally — and if synthesizable they could lead directly to implementation. Synthesis is considerably harder for LSCs than for MSCs, and we tackle it by defining consistency, showing that an entire LSC specification is consistent iff it is satisfiable by a state-based object system, and then synthesizing a satisfying system as a collection of finite state machines or statecharts.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Amon, T., G. Boriello and C. Sequin, “Operation/Event Graphs: A design representation for timing behavior”, Proc.’ 91 Conf. on Computer Hardware Description Language, pp. 241–260, 1991.
Abadi, M., L. Lamport and P. Wolper, “Realizable and unrealizable concurrent program specifications”, Proc. 16th Int. Colloq. on Automata, Languages and Programming, Lecture Notes in Computer Science, vol. 372, Springer-Verlag, pp. 1–17, 1989.
Alur, R., and M. Yannakakis, “Model Checking of Message Sequence Charts”, to appear in Proc. 10th Int. Conf. on Concurrency Theory (CONCUR’99), Eindhoven, Netherlands, August 1999.
Alur, R., K. Etessami and M. Yannakakis, “Inference of Message Sequence Charts”, Proc. 22nd Int. Conf. on Software Engineering (ICSE’00), Limerick, Ireland, June 2000.
Boriello, G., “A new interface specification methodology and its application to transducer synthesis”, Technical Report UCB/CSD 88/430, University of California Berkeley, 1988.
Biermann, A.W., and R. Krishnaswamy, “Constructing Programs from Example Computations”, IEEE Trans. Softw. Eng., SE-2 (1976), 141–153.
Broy, M., and I. Krüger, “Interaction Interfaces — Towards a Scientific Foundation of a Methodological Usage of Message Sequence Charts”, In Formal Engineering Methods, (J. Staples, M.G. Hinchey, and Shaoying Liu, eds), IEEE Computer Society, 1998, pp. 2–15.
Damm, W., and D. Harel, “LSCs: Breathing Life into Message Sequence Charts”, Proc. 3rd IFIP Int. Conf. on Formal Methods for Open Object-based Distributed Systems, (P. Ciancarini, A. Fantechi and R. Gorrieri, eds.), Kluwer Academic Publishers, pp. 293–312, 1999.
Emerson, E.A., “Temporal and modal logic”, Handbook of Theoretical Computer Science, (1990), 997–1072.
Emerson, E.A., and E.M. Clarke, “Using branching time temporal logic to synthesize synchronization skeletons”, Sci. Comp. Prog. 2 (1982), 241–266.
Harel, D., “Statecharts: A Visual Formalism for Complex Systems”, Sci. Comput. Prog. 8 (1987), 231–274. (Preliminary version: Tech. Report CS84-05, The Weizmann Institute of Science, Rehovot, Israel, February 1984.)
Harel, D., “From Play-In Scenarios To Code: An Achievable Dream”, Proc. Fundamental Approaches to Software Engineering (FASE), Lecture Notes in Computer Science, Vol. 1783 (Tom Maibaum, ed.), Springer-Verlag, March 2000, pp. 22–34.
Harel, D., and E. Gery, “Executable Object Modeling with Statecharts”, IEEE Computer, (1997), 31–42.
Harel, D., and H. Kugler, “Synthesizing State-Based Object Systems from LSC Specifications”, 1999, Available as Technical Report MCS99-20, TheWeizmann Institute of Science, Department of Computer Science, Rehovot, Israel, http://www.wisdom.weizmann.ac.il/reports.html.
Harel, D., and O. Kupferman, “On the Inheritance of State-Based Object Behavior”, Proc. 34th Int. Conf. on Component and Object Technology, IEEE Computer Society, Santa Barbara, CA, August 2000.
Jacobson, I., Object-Oriented Software Engineering: A Use Case Driven Approach. Addison-Wesley, Reading, MA, 1992.
Krüger, I., R. Grosu, P. Scholz and M. Broy “From MSCs to Statecharts”, Proc. DIPES’98, Kluwer, 1999.
Koskimies, K., and E. Makinen, “Automatic Synthesis of State Machines from Trace Diagrams”, Software — Practice and Experience 24:7 (1994), 643–658.
Koskimies, K., T. Systa, J. Tuomi and T. Mannisto, “Automated Support for Modeling OO Software”, IEEE Software 15:1 (1998), 87–94.
Kupferman, O., and M.Y. Vardi, “Synthesis with incomplete information”, Proc. 2nd Int. Conf. on Temporal Logic (ICTL97), pp. 91–106, 1997.
Klose, J., and H. Wittke, “Automata Representation of Live Sequence Charts”, manuscript, 2000.
Leue, S., L. Mehrmann and M. Rezai, “Synthesizing ROOM Models from Message Sequence Chart Specifications”, University of Waterloo Tech. Report 98-06, April 1998.
Manna, Z., and R.J. Waldinger, “A deductive approach to program synthesis” ACM Trans. Prog. Lang. Sys. 2 (1980), 90–121.
Pnueli, A., and R. Rosner, “On the Synthesis of a Reactive Module”, Proc. 16th ACM Symp. on Principles of Programming Languages, Austin,TX, January 1989.
Pnueli, A., R. Rosner, “On the Synthesis of an Asynchronous Reactive Module”, Proc. 16th Int. Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, vol. 372, Springer-Verlag, pp. 652–671, 1989.
Pnueli, A., R. Rosner, “Distributed Reactive Systems are Hard to Synthesize”, Proc. 31st IEEE Symp. on Foundations of Computer Science, pp. 746–757, 1990.
Schlor, R. and W. Damm, “Specification and verification of system-level hardware designs using timing diagrams”, Proc. European Conference on Design Automation, Paris, France, IEEE Computer Society Press, pp. 518–524, 1993.
Selic, B., G. Gullekson and P. Ward, Real-Time Object-Oriented Modeling, John Wiley & Sons, New York, 1994.
Documentation of the Unified Modeling Language (UML), available from the Object Management Group (OMG), http://www.omg.org.
Wong-Toi, H., and D.L. Dill, “Synthesizing processes and schedulers from temporal specifications”, In Computer-Aided Verification’ 90 (Clark and Kurshan, eds.), DIMACS Series in Discrete Mathematics and Theoretical Computer Science, volume 3, pp. 177–186, 1991.
Whittle, J. and J. Schumann, “Generating Statechart Designs from Scenarios”, Proc. 22nd Int. Conf. on Software Engineering (ICSE’00), Limerick, Ireland, June 2000.
Z.120 ITU-T Recommendation Z.120: Message Sequence Chart (MSC), ITU-T, Geneva, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Harel, D., Kugler, H. (2001). Synthesizing State-Based Object Systems from LSC Specifications. In: Yu, S., Păun, A. (eds) Implementation and Application of Automata. CIAA 2000. Lecture Notes in Computer Science, vol 2088. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44674-5_1
Download citation
DOI: https://doi.org/10.1007/3-540-44674-5_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42491-8
Online ISBN: 978-3-540-44674-3
eBook Packages: Springer Book Archive