{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T15:07:08Z","timestamp":1773414428275,"version":"3.50.1"},"reference-count":27,"publisher":"MDPI AG","issue":"1","license":[{"start":{"date-parts":[[2025,2,27]],"date-time":"2025-02-27T00:00:00Z","timestamp":1740614400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Software"],"abstract":"<jats:p>The unified modelling language (UML) is an industrial de facto standard for system modelling. It consists of a set of graphical notations (also known as diagrams) and has been used widely in many industrial applications. Although the graphical nature of UML is appealing to system developers, the official documentation of UML does not provide formal semantics for UML diagrams. This makes UML unsuitable for formal verification and, therefore, limited when it comes to the development of safety\/security-critical systems where faults can cause damage to people, properties, or the environment. The UML activity diagram is an important UML graphical notation, which is effective in modelling the dynamic aspects of a system. This paper proposes a formal semantics for UML activity diagrams based on the calculus of context-aware ambients (CCA). An algorithm (semantic function) is proposed that maps any activity diagram onto a process in CCA, which describes the behaviours of the UML activity diagram. This process can then be executed and formally verified using the CCA simulation tool ccaPL and the CCA runtime verification tool ccaRV. Hence, design flaws can be detected and fixed early during the system development lifecycle. The pragmatics of the proposed approach are demonstrated using a case study in e-commerce.<\/jats:p>","DOI":"10.3390\/software4010004","type":"journal-article","created":{"date-parts":[[2025,2,28]],"date-time":"2025-02-28T06:45:42Z","timestamp":1740725142000},"page":"4","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["On the Execution and Runtime Verification of UML Activity Diagrams"],"prefix":"10.3390","volume":"4","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3741-3074","authenticated-orcid":false,"given":"Fran\u00e7ois","family":"Siewe","sequence":"first","affiliation":[{"name":"School of Computer Science and informatics, De Montfort University, Leicester LE1 9BH, UK"}]},{"given":"Guy Merlin","family":"Ngounou","sequence":"additional","affiliation":[{"name":"Department of Computer Engineering, Ecole Nationale Sup\u00e9rieure Polytechnique de Yaound\u00e9, Yaound\u00e9 P.O. Box 8390, Cameroon"}]}],"member":"1968","published-online":{"date-parts":[[2025,2,27]]},"reference":[{"key":"ref_1","unstructured":"Object Management Group (2011). OMG Unified Modeling Language (OMG UML), Superstructure. Version 2.4.1, Object Management Group."},{"key":"ref_2","unstructured":"(2005). Information Technology\u2014Open Distributed Processing\u2014Unified Modeling Language (UML) Version 1.4.3 (Standard No. ISO\/IEC 19501:2005)."},{"key":"ref_3","unstructured":"Li, X., Liu, Z., and Jifeng, H. (2004, January 13\u201316). A formal semantics of UML sequence diagram. Proceedings of the 2004 Australian Software Engineering Conference. Proceedings., Melbourne, Australia."},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"1229","DOI":"10.4304\/jsw.9.5.1229-1236","article-title":"UML-Checker: An Approach for Verifying UML Behavioral Diagrams","volume":"9","author":"Fernandes","year":"2014","journal-title":"J. Softw."},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/j.entcs.2009.09.064","article-title":"Formal Verification and Validation of UML 2.0 Sequence Diagrams using Source and Destination of Messages","volume":"254","author":"Lima","year":"2009","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"ref_6","doi-asserted-by":"crossref","unstructured":"Mokhati, F., Gagnon, P., and Badri, M. (2007, January 11\u201312). Verifying UML Diagrams with Model Checking: A Rewriting Logic Based Approach. Proceedings of the Seventh International Conference on Quality Software (QSIC 2007), Portland, OR, USA.","DOI":"10.1109\/QSIC.2007.4385520"},{"key":"ref_7","first-page":"20","article-title":"A Method for Modeling and Verifying of UML 2.0 Sequence Diagrams using SPIN","volume":"1","author":"Le","year":"2020","journal-title":"J. Sci. Technol. Inf. Secur."},{"key":"ref_8","doi-asserted-by":"crossref","unstructured":"Shah, K., and Grant, E. (2022, January 27\u201329). Towards Simplifying and Formalizing UML Class Diagram Generalization\/Specialization Relationship with Mathematical Set Theory. Proceedings of the 6th International Conference on Information System and Data Mining, ICISDM \u201922, Silicon Valley, CA, USA.","DOI":"10.1145\/3546157.3546171"},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"142461","DOI":"10.1109\/ACCESS.2021.3121222","article-title":"More Than Two Decades of Research on Verification of UML Class Models: A Systematic Literature Review","volume":"9","author":"Shaikh","year":"2021","journal-title":"IEEE Access"},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"597","DOI":"10.1016\/j.jcss.2010.02.003","article-title":"The Calculus of Context-aware Ambients","volume":"77","author":"Siewe","year":"2011","journal-title":"J. Comput. Syst. Sci."},{"key":"ref_11","unstructured":"Siewe, F. (2023, November 23). ccaPL: A CCA Programming Environment. Available online: https:\/\/fsiewe.afrilocode.net\/CCA\/index.html."},{"key":"ref_12","unstructured":"(2023, November 23). AT&T Labs-Research. Graphviz Distribution. Available online: http:\/\/www.research.att.com\/sw\/tools\/graphviz\/download.html."},{"key":"ref_13","doi-asserted-by":"crossref","unstructured":"Colombo, C., and Leucker, M. (2018). Runtime Verification: From Propositional to First-Order Temporal Logic. Runtime Verification, Springer.","DOI":"10.1007\/978-3-030-03769-7"},{"key":"ref_14","doi-asserted-by":"crossref","unstructured":"Bartocci, E., and Falcone, Y. (2018). Introduction to Runtime Verification. Lectures on Runtime Verification: Introductory and Advanced Topics, Springer International Publishing.","DOI":"10.1007\/978-3-319-75632-5"},{"key":"ref_15","doi-asserted-by":"crossref","unstructured":"Colombo, C., and Leucker, M. (2018). Runtime Verification\u201417 Years Later. Runtime Verification, Springer.","DOI":"10.1007\/978-3-030-03769-7"},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1007\/s10270-011-0207-y","article-title":"UML formal semantics: Lessons learned","volume":"10","author":"Broy","year":"2011","journal-title":"Softw. Syst. Model."},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Daw, Z., and Cleaveland, R. (2016). An extensible formal semantics for UML activity diagrams. arXiv.","DOI":"10.1007\/978-3-319-22969-0_25"},{"key":"ref_18","unstructured":"Liggesmeyer, P., Pohl, K., and Goedicke, M. (2005, January 8\u201311). Towards a formal semantics of UML 2.0 activities. Proceedings of the Software Engineering 2005, Essen, Germany."},{"key":"ref_19","doi-asserted-by":"crossref","unstructured":"Siewe, F. (2023, January 27\u201329). Towards the Formal Analysis of UML Activity Diagrams in a Calculus of Context-aware Ambients. Proceedings of the 2023 IEEE 47th Annual Computers, Software, and Applications Conference (COMPSAC), Torino, Italy.","DOI":"10.1109\/COMPSAC57700.2023.00261"},{"key":"ref_20","first-page":"1","article-title":"Synthesis and Consistency Verification of UML Sequence Diagrams with Hierarchical Structure","volume":"6","author":"Matsumoto","year":"2020","journal-title":"Inf. Eng. Express"},{"key":"ref_21","doi-asserted-by":"crossref","unstructured":"Zhou, Z., Wang, L., Cui, Z., Chen, X., and Zhao, J. (2008, January 3\u20135). Jasmine: A Tool for Model-Driven Runtime Verification with UML Behavioral Models. Proceedings of the 2008 11th IEEE High Assurance Systems Engineering Symposium, Nanjing, China.","DOI":"10.1109\/HASE.2008.62"},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"102955","DOI":"10.1016\/j.scico.2023.102955","article-title":"QMaxUSE: A new tool for verifying UML class diagrams and OCL invariants","volume":"228","author":"Wu","year":"2023","journal-title":"Sci. Comput. Program."},{"key":"ref_23","doi-asserted-by":"crossref","first-page":"101911","DOI":"10.1016\/j.sysarc.2020.101911","article-title":"Formal modeling and verification of UML Activity Diagrams (UAD) with FoCaLiZe","volume":"114","author":"Abbas","year":"2021","journal-title":"J. Syst. Archit."},{"key":"ref_24","first-page":"131","article-title":"FMSG: A framework for modeling and verification of a smart grid","volume":"49","author":"Karmakar","year":"2024","journal-title":"Sadhana\u2014Acad. Proc. Eng. Sci."},{"key":"ref_25","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/978-981-16-7167-8_23","article-title":"Mapping UML Activity Diagram into Z Notation","volume":"96","author":"Halder","year":"2022","journal-title":"Lect. Notes Data Eng. Commun. Technol."},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Xu, Z., Sun, F., and Zhang, W. (2024, January 28\u201330). Research on Activity Diagram Testing method based on UML Testing Profile. Proceedings of the 2024 6th International Conference on Electronic Engineering and Informatics (EEI), Chongqing, China.","DOI":"10.1109\/EEI63073.2024.10696704"},{"key":"ref_27","doi-asserted-by":"crossref","unstructured":"Muqsith, M.F., Priyadi, Y., and Astuti, W. (2023, January 9\u201310). UML Artifact Extraction for Activity Diagram Based on Step Performed Using Text Mining: Case Study of SRS Sipranta Application. Proceedings of the 2023 3rd International Conference on Electronic and Electrical Engineering and Intelligent System (ICE3IS), Yogyakarta, Indonesia.","DOI":"10.1109\/ICE3IS59323.2023.10335296"}],"container-title":["Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2674-113X\/4\/1\/4\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T16:43:44Z","timestamp":1760028224000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2674-113X\/4\/1\/4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,2,27]]},"references-count":27,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2025,3]]}},"alternative-id":["software4010004"],"URL":"https:\/\/doi.org\/10.3390\/software4010004","relation":{},"ISSN":["2674-113X"],"issn-type":[{"value":"2674-113X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,2,27]]}}}