Abstract
Models are used for a number of different purposes, from the requirements capture and design of a new system, to the testing of an existing system. Many different modeling languages are available, and the semantics given for the languages vary from informal natural language descriptions to various kinds of mathematical or logical definitions. When choosing a modeling language and accompanying semantics, a number of things need to be taken into consideration, such as who are the users of the models, what is the purpose of the models, what kind of application is being modeled, and what are the essential features that must be captured.
When modeling embedded systems, an essential aspect is the interaction between hardware and software. Hence, we need to capture the behavior of the hardware and software components. For capturing the dynamic behavior of components, modeling languages like UML sequence diagrams, state machines and similar notations are often used. This paper surveys different approaches to formally capturing the semantics of models expressed using languages of this kind.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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
Object Management Group: Unified Modeling Language: Superstructure, version 2.1.1 (non-change bar). OMG Document: formal/2007-02-05 (2005)
International Telecommunication Union: Message Sequence Chart (MSC), ITU-T Recommendation Z.120 (1999)
Damm, W., Harel, D.: LSCs: Breathing life into Message Sequence Charts. Formal Methods in System Design 19, 45–80 (2001)
Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming 8(3), 231–274 (1987)
International Telecommunication Union: Specification and description language (SDL), ITU-T Recommendation Z.100 (2000)
Labinaz, G., Bayoumi, M.M., Rudie, K.: A survey of modeling and control of hybrid systems. Annual Reviews of Control 21, 79–92 (1997)
Giese, H., Henkler, S.: A survey of approaches for the visual model-driven development of next generation software-intensive systems. Journal of Visual Languages and Computing 17(6), 528–550 (2006)
McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: Proceedings of the IEEE Symposium on Research in Security and Privacy, pp. 79–93. IEEE Computer Society, Los Alamitos (1994)
Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters 21(4), 181–185 (1985)
Schneider, F.B.: Enforceable security policies. ACM Transactions on Information System Security 3(1), 30–50 (2000)
Harel, D., Rumpe, B.: Meaningful modeling: What’s the semantics of “semantics”? Computer 37(10), 64–72 (2004)
Prinz, A.: Formal semantics of specification languages. Telektronikk (4), 146–155 (2000)
Fecher, H., Schönborn, J., Kyas, M., de Roever, W.P.: 29 new unclarities in the semantics of UML 2.0 state machines. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 52–65. Springer, Heidelberg (2005)
Schmidt, D.A.: Denotational semantics. A methodology for language development. William C. Brown (1988)
Hoare, C.A.R., Jifeng, H.: Unifying theories of programming. Prentice-Hall, Englewood Cliffs (1998)
Object Management Group: Unified Modeling Language Specification, version 1.4. OMG Document: formal/2001-09-67 (2001)
Facchi, C.: Formal semantics of Time Sequence Diagrams. Technical report TUM-I9540, Technische Universität München (1995)
International Telecommunication Union: Information technology – Open Systems Interconnection – Basic reference model: Conventions for the definition of OSI services, ITU-T Recommendation X.210 (1993)
Bræk, R., Gorman, J., Haugen, Ø., Møller-Pedersen, B., Melby, G., Sanders, R., Stålhane, T.: TIMe: The Integrated Method. Electronic Textbook v4.0. SINTEF (1999)
International Telecommunication Union: Message Sequence Chart (MSC), ITU-T Recommendation Z.120 (1996)
International Telecommunication Union: Message Sequence Chart (MSC), ITU-T Recommendation Z.120, Annex B: Formal semantics of Message Sequence Charts (1998)
Haugen, Ø.: Comparing UML 2.0 Interactions and MSC-2000. In: Amyot, D., Williams, A.W. (eds.) SAM 2004. LNCS, vol. 3319, pp. 65–79. Springer, Heidelberg (2005)
Object Management Group: UML Testing Profile, version 1.0. OMG Document: formal/2005-07-07 (2005)
Object Management Group: UML Profile for Schedulability, Performance, and Time Specification, version 1.1. OMG Document: formal/2005-01-02 (2005)
Katoen, J.P., Lambert, L.: Pomsets for Message Sequence Charts. In: Formale Beschreibungstechniken für Verteilte Systeme, pp. 197–208. Shaker (1998)
Alur, J., Yannakakis, M.: Model checking of Message Sequence Charts. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 98–113. Springer, Heidelberg (1999)
Krüger, I.H.: Distributed system design with Message Sequence Charts. PhD thesis, Technische Universität München (2000)
Haugen, Ø., Husa, K.E., Runde, R.K., Stølen, K.: STAIRS towards formal design with sequence diagrams. Software and Systems Modeling 4(4), 355–367 (2005)
Seehusen, F., Solhaug, B., Stølen, K.: Adherence preserving refinement of trace-set properties in STAIRS: Exemplified for information flow properties and policies. Software and Systems Modeling 8(1), 45–65 (2009)
Störrle, H.: Assert, negate and refinement in UML 2 interactions. In: 2nd International Workshop on Critical Systems Development with UML (CSD-UML 2003), Technische Universität München, pp. 79–93 (2003)
Störrle, H.: Semantics of interaction in UML 2.0. In: IEEE Symposium on Human Centric Computing Languages and Environments (HCC 2003), pp. 129–136. IEEE Computer Society, Los Alamitos (2003)
Störrle, H.: Trace semantics of interactions in UML 2.0. Technical report TR 0403, Institut für Informatik, der Ludwig-Maximilians-Universität München (2004)
Cengarle, M.V., Knapp, A.: UML 2.0 interactions: Semantics and refinement. In: 3rd International Workshop on Critical Systems Development with UML (CSD-UML 2004), Technische Universität München, pp. 85–99 (2004)
Küster-Filipe, J.: Modelling concurrent interactions. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 304–318. Springer, Heidelberg (2004)
Alur, R., Holzmann, G.J., Peled, D.: An analyzer for Message Sequence Charts. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 35–48. Springer, Heidelberg (1996)
Alur, R., Etessami, K., Yannakakis, M.: Inference of Message Sequence Charts. IEEE Transactions on Software Engineering 29(7), 623–633 (2003)
Zheng, T., Khendek, F., Hélouët, L.: A semantics for timed MSC. Electronic Notes in Theoretical Computer Science 65(7), 85–99 (2002)
Zheng, T., Khendek, F., Parreaux, B.: Refining timed MSCs. In: Reed, R., Reed, J. (eds.) SDL 2003. LNCS, vol. 2708, pp. 234–250. Springer, Heidelberg (2003)
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)
Runde, R.K.: STAIRS - Understanding and developing specifications expressed as UML interaction diagrams. PhD thesis, Faculty of Mathematics and Natural Sciences, University of Oslo (2007)
Faltin, N., Lambert, L., Mitschele-Thiel, A., Slomka, F.: An annotational extension of Message Sequence Charts to support performance engineering. In: 8th International SDL Forum: Time for Testing, SDL, MSC and Trends (SDL 1997), pp. 307–322. Elsevier, Amsterdam (1997)
Lambert, L.: PMSC for performance evaluation. In: 1st Workshop on Performance and Time in SDL/MSC, pp. 70–80 (1998)
Refsdal, A., Husa, K.E., Stølen, K.: Specification and refinement of soft real-time requirements using sequence diagrams. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 32–48. Springer, Heidelberg (2005)
Refsdal, A., Runde, R.K., Stølen, K.: Underspecification, inherent nondeterminism and probability in sequence diagrams. In: Gorrieri, R., Wehrheim, H. (eds.) FMOODS 2006. LNCS, vol. 4037, pp. 138–155. Springer, Heidelberg (2006)
Refsdal, A.: Specifying computer systems with probabilistic sequence diagrams. PhD thesis, Faculty of Mathematics and Natural Sciences, University of Oslo (2008)
Mauw, S.: The formalization of Message Sequence Charts. Computer Networks and ISDN Systems 28(1), 1643–1657 (1996)
Mauw, S., Reniers, M.A.: An algebraic semantics of Basic Message Sequence Charts. The Computer Journal 37(4), 269–278 (1994)
Okazaki, M., Aoki, T., Katayama, T.: Formalizing sequence diagrams and state machines using Concurrent Regular Expression. In: 2nd International Workshop on Scenarios and State Machines: Models, Algorithms, and Tools, SCESM 2003 (2003)
Mauw, S., Reniers, M.A.: Operational semantics for MSC’96. Computer Networks 31(17), 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)
Letichevsky, A.A., Kapitonova, J.V., Kotlyarov, V.P., Volkov, V.A., Letichevsky Jr., A.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)
Alur, R., Etessami, K., Yannakakis, M.: Realizability and verification of MSC graphs. Theoretical Computer Science 331(1), 97–114 (2005)
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(1), 37–85 (2004)
Graubmann, P., Rudolph, E., Grabowski, J.: Towards a Petri net based semantics for Message Sequence Charts. In: 6th International SDL Forum: Using objects (SDL 1993), pp. 179–190. Elsevier, Amsterdam (1993)
Heymer, S.: A semantics for MSC based on Petri net components. In: 4th International SDL and MSC Workshop (SAM 2000), pp. 262–275 (2000)
Sgroi, M., Kondratyev, A., Watanabe, Y., Lavagno, L., Sangiovanni-Vincentelli, A.: Synthesis of Petri nets from Message Sequence Charts specifications for protocol design. In: Design, Analysis and Simulation of Distributed Systems Symposium (DASD 2004), pp. 193–199 (2004)
Gunter, E.L., Muscholl, A., Peled, D.: Compositional Message Sequence Charts. International Journal on Software Tools for Technology Transfer 5(1), 78–89 (2003)
Bernardi, S., Donatelli, S., Merseguer, J.: From UML sequence diagrams and statecharts to analysable Petri net models. In: 3rd International Workshop on Software and Performance (WOSP 2002), pp. 35–45. ACM Press, New York (2002)
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)
Lund, M.S.: Operational analysis of sequence diagram specifications. PhD thesis, Faculty of Mathematics and Natural Sciences, University of Oslo (2008)
Lund, M.S., Stølen, K.: 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. LNCS, vol. 4085, pp. 380–395. Springer, Heidelberg (2006)
Cengarle, M.V., Knapp, A.: Operational semantics of UML 2.0 interactions. Technical report TUM-I0505, Technische Universität München (2005)
Mühlberger, H.: Eine verteile operationale Semantik für UML 2.0-Interaktionen. Diplomarbeit, Institut für Informatik, der Ludwig-Maximilians-Universität München (2007)
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)
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)
Harel, D., Marelly, R.: Come, let’s play: Scenario-based programming using LSCs and the Play-Engine. Springer, Heidelberg (2003)
Harel, D., Thiagarajan, P.S.: Message Sequence Charts. In: Lavagano, L., Martin, G., Selic, B. (eds.) UML for real. Design of embedded real-time systems, pp. 77–105. Kluwer, Dordrecht (2003)
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)
Sengupta, B., Cleaveland, R.: Triggered Message Sequence Charts. SIGSOFT Software Engineering Notes 27(6), 167–176 (2002)
Sengupta, B., Cleaveland, R.: Triggered Message Sequence Carts. IEEE Transactions on Software Engineering 32(8) (2006)
Kosiuczenko, P., Wirsing, M.: Towards an integration of Message Sequence Charts and Timed Maude. Journal of Integrated Design & Process Science 5(1), 23–44 (2001)
Crane, M.L., Dingel, J.: On the semantics of UML state machines: Categorization and comparison. Technical report 2005-501, School of Computing, Queens’s University, Kingston (2005)
Broy, M., Cengarle, M.V., Rumpe, B.: Towards a system model for UML, the structural data model. Technical report TUM-I0612, Technische Universität München (2006)
Broy, M., Cengarle, M.V., Rumpe, B.: Towards a system model for UML, part 2: The control model. Technical report TUM-I0710, Technische Universität München (2007)
Broy, M., Cengarle, M.V., Rumpe, B.: Towards a system model for UML, part 3: The state machine model. Technical report TUM-I0711, Technische Universität München (2007)
Broy, M., Stølen, K.: Specification and development of interactive systems. In: FOCUS on streams, interface, and refinement. Springer, Heidelberg (2001)
Simons, A.J.H.: On the compositional properties of UML statechart diagrams. In: Rigorous Object-Oriented Methods (ROOM 2000), Workshops in Computing, BCS (2000) (2000)
Rossi, C., Enciso, M., de Guzmán, I.P.: Formalization of UML state machines using temporal logic. Software and Systems Modeling 3(1), 31–54 (2004)
Hinkel, U.: Verification of SDL specifications on the basis of stream semantics. In: 1st Workshop of the SDL Forum Society on SDL and MSC (SAM 1998), pp. 241–250 (1998)
Holz, E., Stølen, K.: An attempt to embed a restricted version of SDL as a target language in Focus. In: Formal Description Techniques VII (FORTE 1994), pp. 324–339. Chapman and Hall, Boca Raton (1994)
Harel, D., Naamad, A.: The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology 5(4), 293–333 (1996)
Harel, D., Lachover, H., Naamad, A., Pnueli, A., Politi, M., Sherman, R., Shtull-Trauring, A., Trakhtenbrot, M.: STATEMATE: A working environment for the development of complex reactive systems. IEEE Transactions on Software Engineering 16(4), 403–414 (1990)
Gurevich, Y.: Evolving algebras 1993: Lipari guide. In: Specification and Validation Methods, pp. 9–36. Oxford University Press, Oxford (1995)
Börger, E., Cavarra, A., Riccobene, E.: On formalizing UML state machines using ASMs. Information and Software Technology 46(5), 287–292 (2004)
Börger, E., Cavarra, A., Riccobene, E.: Modeling the dynamics of UML state machines. In: International Workshop on Abstract State Machines, Theory and Applications, pp. 223–241. Springer, Heidelberg (2000)
Börger, E., Cavarra, A., Riccobene, E.: Modeling the meaning of transitions from and to concurrent states in UML state machines. In: 2003 ACM Symposium on Applied Computing, pp. 1086–1091. ACM Press, New York (2003)
Jürjens, J.: A UML statecharts semantics with message-passing. In: 2002 ACM Symposium on Applied Computing, pp. 1009–1013. ACM Press, New York (2002)
Jürjens, J.: Secure systems development with UML. Springer, Heidelberg (2005)
von der Beeck, M.: A structured operational semantics for UML-statecharts. Software and Systems Modeling 1(2), 130–141 (2002)
Knapp, A., Merz, S., Rauh, C.: Model checking timed UML state machines and collaborations. In: 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 395–416. Springer, Heidelberg (2002)
Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer 1, 134–152 (1997)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Lüttgen, G., von der Beeck, M., Cleaveland, R.: A compositional approach to statecharts semantics. Technical report, Institute for Computer Applications in Science and Engineering (2000)
Jansen, D.N., Hermanns, H., Katoen, J.P.: A QoS-oriented extension of UML statecharts. In: Stevens, P., Whittle, J., Booch, G. (eds.) UML 2003. LNCS, vol. 2863, pp. 76–91. Springer, Heidelberg (2003)
Jansen, D.N., Hermanns, H.: Qos modelling and analysis with UML-statecharts: the Stocharts approach. SIGMETRICS Performance Evaluation Review 32(4), 28–33 (2005)
Eshuis, R., Wieringa, R.: Requirements-level semantics for UML statecharts. In: 4th International Conference on Formal Methods for Open Object-Based Distributed Systems IV, pp. 121–140. Kluwer, Dordrecht (2000)
Huszerl, G., Kosmidis, K., Cin, M.D., Majzik, I., Pataricza, A.: Quantitative analysis of UML statechart models of dependable systems. The Computer Journal 45(3), 260–277 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Lund, M.S., Refsdal, A., Stølen, K. (2010). 4 Semantics of UML Models for Dynamic Behavior. In: Giese, H., Karsai, G., Lee, E., Rumpe, B., Schätz, B. (eds) Model-Based Engineering of Embedded Real-Time Systems. MBEERTS 2007. Lecture Notes in Computer Science, vol 6100. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16277-0_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-16277-0_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16276-3
Online ISBN: 978-3-642-16277-0
eBook Packages: Computer ScienceComputer Science (R0)