Abstract
UML sequence diagrams is a specification language that has proved itself to be of great value in system development. When put to applications such as simulation, testing and other kinds of automated analysis there is a need for formal semantics. Such methods of automated analysis are by nature operational, and this motivates formalizing an operational semantics. In this paper we present an operational semantics for UML 2.0 sequence diagrams that we believe gives a solid starting point for developing methods for automated analysis. The operational semantics has been proved to be sound and complete with respect to a denotational semantics for the same language. It handles negative behavior as well as potential and mandatory choice. We are not aware of any other operational semantics for sequence diagrams of this strength.
The work of this paper was conducted within and funded by the Basic ICT Research project SARDAS (15295/431) under the Research Council of Norway. We would like to thank Rolv Bræk, Manfred Broy, Kathrin Greiner, Øystein Haugen, Birger Møller-Pedersen, Atle Refsdal, Ragnhild Kobro Runde, Ina Schieferdecker and Thomas Weigert for useful comments on this work.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Object Management Group: Unified Modeling Language: Superstructure, version 2.0, OMG Document: formal/2005-07-04 (2005)
International Telecommunication Union: Message Sequence Chart (MSC), ITU-T Recommendation Z.120 (1999)
Haugen, Ø., Husa, K.E., Runde, R.K., Stølen, K.: STAIRS towards formal design with sequence diagrams. Software and Systems Modeling 4, 355–367 (2005)
Haugen, Ø., Husa, K.E., Runde, R.K., Stølen, K.: Why timed sequence diagrams require three-event semantics. In: Leue, S., Systä, T.J. (eds.) Scenarios: Models, Transformations and Tools. LNCS, vol. 3466, pp. 1–25. Springer, Heidelberg (2005)
Haugen, Ø., Husa, K.E., Runde, R.K., Stølen, K.: Why timed sequence diagrams require three-event semantics. Research report 309, Department of Informatics, University of Oslo (2004) (revised June 2005)
Lund, M.S., Stølen, K.: A fully general operational semantics for UML sequence diagrams with potential and mandatory choice. Research report 330, Department of Informatics, University of Oslo (2006)
Jonsson, B., Padilla, G.: An execution semantics for MSC-2000. In: Reed, R., Reed, J. (eds.) SDL 2001. LNCS, vol. 2078, pp. 365–378. Springer, Heidelberg (2001)
Harel, D., Marelly, R.: Come, let’s play: Scenario-based programming using LSCs and the Play-Engine. Springer, Heidelberg (2003)
Cavarra, A., Küster-Filipe, J.: Formalizing liveness-enriched sequence diagrams using ASMs. In: Zimmermann, W., Thalheim, B. (eds.) ASM 2004. LNCS, vol. 3052, pp. 67–77. Springer, Heidelberg (2004)
Harel, D., Maoz, S.: Assert and negate revisited: Modal semantics for UML sequence diagrams. In: 5th International Workshop on Scenarios and State Machines: Models, Algorithms, and Tools (SCESM 2006), pp. 13–19. ACM Press, New York (2006)
Grosu, R., Smolka, S.A.: Safety-liveness semantics for UML 2.0 sequence diagrams. In: 5th International Conference on Application of Concurrency to System Design (ACSD 2005), pp. 6–14. IEEE Computer Society, Los Alamitos (2005)
Letichevsky, A., Kapitonova, J., Kotlyarov, V., Volkov, V., Letichevsky, A., Weigert, T.: Semantics of Message Sequence Charts. In: Prinz, A., Reed, R., Reed, J. (eds.) SDL 2005. LNCS, vol. 3530, pp. 117–132. Springer, Heidelberg (2005)
Cengarle, M.V., Knapp, A.: Operational semantics of UML 2.0 interactions. Technical report TUM-I0505, Technische Universität München (2005)
Alur, R., Etessami, K., Yannakakis, M.: Inference of Message Sequence Charts. IEEE Transactions on Software Engineering 29, 623–633 (2003)
Alur, R., Etessami, K., Yannakakis, M.: Realizability and verification of MSC graphs. Theoretical Computer Science 331, 97–114 (2005)
Mauw, S., Reniers, M.A.: Operational semantics for MSC 1996. Computer Networks 31, 1785–1799 (1999)
Mauw, S., Reniers, M.A.: High-level Message Sequence Charts. In: 8th International SDL Forum: Time for Testing, SDL, MSC and Trends (SDL 1997), pp. 291–306. Elsevier, Amsterdam (1997)
International Telecommunication Union: Message Sequence Chart (MSC), ITU-T Recommendation Z.120, Annex B: Formal semantics of Message Sequence Charts (1998)
Uchitel, S., Kramer, J., Magee, J.: Incremental elaboration of scenario-based specification and behavior models using implied scenarios. ACM Transactions on Software Engineering and Methodology 13, 37–85 (2004)
Kosiuczenko, P., Wirsing, M.: Towards an integration of Message Sequence Charts and Timed Maude. Journal of Integrated Design & Process Science 5, 23–44 (2001)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Maude Manual (Version 2.2). SRI International, Menlo Park (2005)
Lund, M.S., Stølen, K.: Deriving tests from UML 2.0 sequence diagrams with neg and assert. In: 1st International Workshop on Automation of Software Test (AST 2006), pp. 22–28. ACM Press, New York (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lund, M.S., Stølen, K. (2006). A Fully General Operational Semantics for UML 2.0 Sequence Diagrams with Potential and Mandatory Choice. In: Misra, J., Nipkow, T., Sekerinski, E. (eds) FM 2006: Formal Methods. FM 2006. Lecture Notes in Computer Science, vol 4085. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11813040_26
Download citation
DOI: https://doi.org/10.1007/11813040_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37215-8
Online ISBN: 978-3-540-37216-5
eBook Packages: Computer ScienceComputer Science (R0)