Top

Published in:

2025 | OriginalPaper | Chapter

An Integrated Framework for Analysing, Simulating and Testing UML Models

Authors : Gustavo Carvalho, José Dihego, Augusto Sampaio

Published in: Formal Methods: Foundations and Applications

Publisher: Springer Nature Switzerland

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

UML is widely adopted for modelling object-oriented software systems, including diagrams that cover the several facets of the entire development life cycle. Approaches to formal semantics of UML tend to concentrate on individual diagrams and, so far, no complete, standard, semantics is available. Here, we explore a different path and define a natural-language semantics for a component UML model that embodies state machines and composite structure diagrams. We then integrate with the NAT2TEST strategy to provide means for analysis (via model checking and theorem proving), simulation and testing. The integration is based on a systematic process (mapping rules), and its soundness has been validated considering an independent reference formal semantics. The developed tool support automates the translation from UML models to natural-language requirements directly based on the proposed mapping rules. We illustrate our contributions and tool support with respect to two case studies: the classical Dijkstra’s dining philosophers problem, and a distributed ring-buffer model.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Verifying Integrated Designs of UML State Machines and Activities Using CSP

next chapter Brzozowski’s Algorithm for Automata Minimization Verified in Coq

Link: https://cocotec.io/fdr/manual/cspm/prelude.html#compressions.

Link: https://cocotec.io/fdr/manual/examples/index.html#dining-philosophers.

Link: https://ttool.telecom-paris.fr/.

André, E., Liu, S., Liu, Y., Choppy, C., Sun, J., Dong, J.S.: Formalizing UML state machines for automated verification - a survey. ACM Comput. Surv. 55(13s) (2023). https://doi.org/10.1145/3579821

Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-662-07964-5CrossRef

Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language User Guide. Addison-Wesley, Reading (1999)

Calvino., A., Apvrille., L.: Direct model-checking of SysML models. In: Proceedings of the 9th International Conference on Model-Driven Engineering and Software Development - MODELSWARD, pp. 216–223. INSTICC, SciTePress (2021). https://doi.org/10.5220/0010256302160223

Carvalho, G., Barros, F., Carvalho, A., Cavalcanti, A., Mota, A., Sampaio, A.: NAT2TEST tool: from natural language requirements to test cases based on CSP. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 283–290. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22969-0_20CrossRef

Carvalho, G., Cavalcanti, A., Sampaio, A.: Modelling timed reactive systems from natural-language requirements. Form. Asp. Comput. 28(5), 725–765 (2016). https://doi.org/10.1007/s00165-016-0387-xMathSciNetCrossRef

Carvalho, G., Dihego, J., Sampaio, A.: Artefact associated with this paper: “an integrated framework for analysing, simulating and testing UML models” (2024). https://zenodo.org/doi/10.5281/zenodo.13323735

Carvalho, G., Meira, I.: Validating, verifying and testing timed data-flow reactive systems in Coq from controlled natural-language requirements. Sci. Comput. Program. 201, 102537 (2021). https://doi.org/10.1016/j.scico.2020.102537, https://www.sciencedirect.com/science/article/pii/S0167642320301453

Carvalho, G., Sampaio, A., Mota, A.: A CSP timed input-output relation and a strategy for mechanised conformance verification. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 148–164. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-41202-8_11CrossRef

10.

Change Vision, Inc.: Astah UML User’s Guide (nd). https://astah.net/support/astah-uml/. Accessed 25 June 2024

11.

Chen, Z., Liu, Z., Ravn, A.P., Stolz, V., Zhan, N.: Refinement and verification in component-based model-driven design. Sci. Comput. Program. 74(4), 168–196 (2009). https://doi.org/10.1016/j.scico.2008.08.003, https://www.sciencedirect.com/science/article/pii/S0167642308000890. Special Issue on the Grand Challenge

12.

Cicchetti, A., et sl.: CHESS: a model-driven engineering tool environment for aiding the development of complex industrial systems. In: 2012 Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering, pp. 362–365 (2012). https://doi.org/10.1145/2351676.2351748

13.

Ciccozzi, F., Malavolta, I., Selic, B.: Execution of UML models: a systematic review of research and practice. Softw. Syst. Model. 18(3), 2313–2360 (2019). https://doi.org/10.1007/s10270-018-0675-4

14.

de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24CrossRef

15.

Dijkstra, E.W.: Solution of a problem in concurrent programming control. Commun. ACM 8, 569 (1965). https://doi.org/10.1145/365559.365617CrossRef

16.

Elekes, M., Molnár, V., Micskei, Z.: To do or not to do: semantics and patterns for do activities in UML PSSM state machines. IEEE Trans. Softw. Eng. 50(8), 2124–2141 (2024). https://doi.org/10.1109/TSE.2024.3422845CrossRef

17.

Falcão, F., Lima, L., Sampaio, A., Antonino, P.: A formal component model for UML based on CSP aiming at compositional verification. Softw. Syst. Model. 23(3), 765–798 (2024). https://doi.org/10.1007/S10270-023-01127-ZCrossRef

18.

Graics, B., Molnár, V., Vörös, A., Majzik, I., Varró, D.: Mixed-semantics composition of statecharts for the component-based design of reactive systems. Softw. Syst. Model. 19(6), 1483–1517 (2020). https://doi.org/10.1007/s10270-020-00806-5CrossRef

19.

Graics, B., Mondok, M., Molnár, V., Majzik, I.: Model-based testing of asynchronously communicating distributed controllers. In: Cámara, J., Jongmans, S.S. (eds.) FACS 2023. LNCS, vol. 14485, pp. 23–44. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-52183-6_2CrossRef

20.

Hoare, C.: Communicating Sequential Processes. Prentice-Hall International (1985)

21.

Horváth, B., et al.: Pragmatic verification and validation of industrial executable SysML models. Syst. Eng. 26(6), 693–714 (2023). https://doi.org/10.1002/sys.21679, https://incose.onlinelibrary.wiley.com/doi/abs/10.1002/sys.21679

22.

Lampropoulos, L., Pierce, B.C.: QuickChick: Property-Based Testing in Coq, Software Foundations, vol. 4. Electronic textbook (2023). http://softwarefoundations.cis.upenn.edu. Version 1.3.2

23.

Lima, L., et al.: An integrated semantics for reasoning about SysML design models using refinement. Softw. Syst. Model. 16(3), 875–902 (2017). https://doi.org/10.1007/s10270-015-0492-yCrossRef

24.

Malavolta, I., Lago, P., Muccini, H., Pelliccione, P., Tang, A.: What industry needs from architectural languages: a survey. IEEE Trans. Softw. Eng. 39(6), 869–891 (2013)CrossRef

25.

Molnár, V., Graics, B., Vörös, A., Majzik, I., Varró, D.: The gamma statechart composition framework: Design, verification and code generation for component-based reactive systems. In: Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings, ICSE 2018, pp. 113–116. Association for Computing Machinery, New York (2018). https://doi.org/10.1145/3183440.3183489

26.

Object Management Group (OMG): UML Resource Page. https://www.omg.org/spec/UML/. Accessed 12 June 2024

27.

Object Management Group (OMG): Semantics of a Foundational Subset for Executable UML Models, Version 1.3. OMG Document Number formal/17-07-02 (2017). https://www.omg.org/spec/FUML/1.3/

28.

Object Management Group (OMG): Precise Semantics of UML Composite Structures, Specification v1.2. OMG Document Number: formal/19-05-01 (2019). https://www.omg.org/spec/PSCS/1.2/

29.

Object Management Group (OMG): Precise Semantics of UML State Machines, Specification v1.0. OMG Document Number: formal/19-05-01 (2019). https://www.omg.org/spec/PSSM/1.0/

30.

Roscoe, A.: The Theory and Practice of Concurrency. Prentice Hall (1997)

31.

Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual. Pearson Higher Education (2004)

Title: An Integrated Framework for Analysing, Simulating and Testing UML Models
Authors: Gustavo Carvalho
José Dihego
Augusto Sampaio
Publisher: Springer Nature Switzerland
Book: Formal Methods: Foundations and Applications
Print ISBN: 978-3-031-78115-5

Electronic ISBN: 978-3-031-78116-2

Copyright Year: 2025
DOI: https://doi.org/10.1007/978-3-031-78116-2_6

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"