Abstract
Interaction languages such as MSC are often associated with formal semantics by means of translations into distinct behavioral formalisms such as automatas or Petri nets. In contrast to translational approaches we propose an operational approach. Its principle is to identify which elementary communication actions can be immediately executed, and then to compute, for every such action, a new interaction representing the possible continuations to its execution. We also define an algorithm for checking the validity of execution traces (i.e. whether or not they belong to an interaction’s semantics). Algorithms for semantic computation and trace validity are analyzed by means of experiments.
Chapter PDF
Similar content being viewed by others
References
Alur, R., Yannakakis, M.: Model checking of message sequence charts. In: CONCUR ’99: Concurrency Theory. Lecture Notes in Computer Science, vol. 1664, pp. 114–129. Springer (1999)
Bannour, B., Gaston, C., Servat, D.: Eliciting unitary constraints from timed sequence diagram with symbolic techniques: Application to testing. In: 2011 18th Asia-Pacific Software Engineering Conference. pp. 219–226 (2011)
Cengarle, M., Knapp, A.: An institution for uml 2.0 interactions (01 2008)
Comon, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (10 2007)
Custódio Soares, J.a.A., Lima, B., Pascoal Faria, J.a.: Automatic model transformation from uml sequence diagrams to coloured petri nets. In: Proceedings of the 6th International Conference on Model-Driven Engineering and Software Development. p. 668–679. MODELSWARD 2018, SCITEPRESS - Science and Technology Publications, Lda, Setubal, PRT (2018). https://doi.org/10.5220/0006731806680679
Damm, W., Harel, D.: Lscs: Breathing life into message sequence charts. Formal Methods in System Design 19(1), 45–80 (2001)
Dershowitz, N., Jouannaud, J.P.: Handbook of theoretical computer science (vol. b). chap. Rewrite Systems, pp. 243–320. MIT Press, Cambridge, MA, USA (1990)
Eichner, C., Fleischhack, H., Meyer, R., Schrimpf, U., Stehno, C.: Compositional semantics for uml 2.0 sequence diagrams using petri nets. In: Prinz, A., Reed, R., Reed, J. (eds.) SDL 2005: Model Driven, pp. 133–148. Springer Berlin Heidelberg, Berlin Heidelberg (2005)
Engels, A., Mauw, S., Reniers, M.: A hierarchy of communication models for message sequence charts. Science of Computer Programming 44(3), 253–292 (2002). https://doi.org/10.1016/S0167-6423(02)00022-9
Faria, J.P., Paiva, A.C.R.: A toolset for conformance testing against uml sequence diagrams based on event-driven colored petri nets. International Journal on Software Tools for Technology Transfer 18(3), 285–304 (2016)
Firley, T., Huhn, M., Diethers, K., Gehrke, T., Goltz, U.: Timed sequence diagrams and tool-based analysis - A case study. In: UML’99: The Unified Modeling Language - Beyond the Standard. Lecture Notes in Computer Science, vol. 1723, pp. 645–660. Springer (1999)
Gérard, S., Dumoulin, C., Tessier, P., Selic, B.: Papyrus: A UML2 Tool for Domain-Specific Language Modeling, pp. 361–368. Springer, Berlin Heidelberg, Berlin, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16277-0_19
Harel, D., Maoz, S.: Assert and negate revisited: Modal semantics for UML sequence diagrams. Software and Systems Modeling 7(2), 237–252 (2008)
Haugen, O., 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)
Hussein, M., Nouacer, R., Radermacher, A., Puccetti, A., Gaston, C., Rapin, N.: An end-to-end framework for safe software development. Microprocessors and Microsystems 62, 41–49 (2018). https://doi.org/10.1016/j.micpro.2018.07.004
Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems. International Journal on Software Tools for Technology Transfer 9(3), 213–254 (2007). https://doi.org/10.1007/s10009-007-0038-x
Knapp, A., Mossakowski, T.: UML Interactions Meet State Machines - An Institutional Approach. In: 7th Conf. on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), vol. 72, pp. 15:1–15:15. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017)
Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer 1(1), 134–152 (Dec 1997). https://doi.org/10.1007/s100090050010
Longuet, D.: Global and local testing from message sequence charts. In: Proceedings of the ACM Symposium on Applied Computing, SAC 2012. pp. 1332–1338. ACM (2012)
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: Formal Methods. pp. 380–395. Springer Berlin Heidelberg, Berlin, Heidelberg (2006)
Micskei, Z., Waeselynck, H.: The many meanings of uml 2 sequence diagrams: a survey. Software & Systems Modeling 10(4), 489–514 (2011)
OASIS: Mqtt version 3.1.1 (12 2015)
OMG: Unified Modeling Language v2.5.1 (12 2017)
Plotkin, G.D.: An operational semantics for CSP. In: Formal Description of Programming Concepts : Proceedings of the IFIP Working Conference on Formal Description of Programming Concepts- II. pp. 199–226. North-Holland (1983)
S., M., M. A., R.: High-level message sequence charts. In: SDL ’97 Time for Testing, SDL, MSC and Trends - 8th International SDL Forum, Proceedings. pp. 291–306. Elsevier (1997)
S., M., M. A., R.: Operational semantics for msc. Computer Networks 31(17), 1785–1799 (1999)
Storrle, H.: Semantics of interactions in uml 2.0. In: IEEE Symposium on Human Centric Computing Languages and Environments, 2003. Proceedings. 2003. pp. 129–136 (Oct 2003). https://doi.org/10.1109/HCC.2003.1260216
Waeselynck, H., Micskei, Z., Rivière, N., Hamvas, Á., Nitu, I.: Termos: A formal language for scenarios in mobile computing systems. In: Sénac, P., Ott, M., Seneviratne, A. (eds.) Mobile and Ubiquitous Systems: Computing, Networking, and Services, pp. 285–296. Springer Berlin Heidelberg, Berlin, Heidelberg (2012)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Mahe, E., Gaston, C., Gall, P.L. (2020). Revisiting Semantics of Interactions for Trace Validity Analysis. In: Wehrheim, H., Cabot, J. (eds) Fundamental Approaches to Software Engineering. FASE 2020. Lecture Notes in Computer Science(), vol 12076. Springer, Cham. https://doi.org/10.1007/978-3-030-45234-6_24
Download citation
DOI: https://doi.org/10.1007/978-3-030-45234-6_24
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45233-9
Online ISBN: 978-3-030-45234-6
eBook Packages: Computer ScienceComputer Science (R0)