{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T19:29:48Z","timestamp":1771702188265,"version":"3.50.1"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2016,9,1]],"date-time":"2016-09-01T00:00:00Z","timestamp":1472688000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>With the increasing complexity of dynamic concurrent systems, a phase of formal specification and formal verification is needed. UML state machines are widely used to specify dynamic systems behaviours. However, the official semantics of UML is described in a semi-formal manner, which renders the formal verification of complex systems delicate. In this paper, we propose a formalisation of UML state machines using coloured Petri nets. We consider in particular concurrent aspects (orthogonal regions, forks, joins, variables), the hierarchy induced by composite states and their associated activities, external, local or inter-level transitions, entry\/exit\/do behaviours, transition priorities, and shallow history pseudostates. We use a CD player as a motivating example, and run various verifications using CPN Tools.<\/jats:p>","DOI":"10.1007\/s00165-016-0388-9","type":"journal-article","created":{"date-parts":[[2016,8,12]],"date-time":"2016-08-12T07:25:19Z","timestamp":1470986719000},"page":"805-845","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Formalising concurrent UML state machines using coloured Petri nets"],"prefix":"10.1145","volume":"28","author":[{"given":"\u00c9tienne","family":"Andr\u00e9","sequence":"first","affiliation":[{"name":"Universit\u00e9 Paris 13, Sorbonne Paris Cit\u00e9, LIPN, CNRS, UMR 7030, 93430, Villetaneuse, France"}]},{"given":"Mohamed Mahdi","family":"Benmoussa","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris 13, Sorbonne Paris Cit\u00e9, LIPN, CNRS, UMR 7030, 93430, Villetaneuse, France"}]},{"given":"Christine","family":"Choppy","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris 13, Sorbonne Paris Cit\u00e9, LIPN, CNRS, UMR 7030, 93430, Villetaneuse, France"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Andr\u00e9 \u00c9 Benmoussa MM Choppy C (2014) Formalising concurrent UML state machines using coloured Petri nets. In: Proceedings of the 6th international conference on knowledge and systems engineering (KSE\u201914) volume 326 of Advances in intelligent systems and computing. Springer pp 473\u2013486","DOI":"10.1007\/978-3-319-11680-8_38"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Andr\u00e9 \u00c9 Benmoussa MM Choppy C (2014) Translating UML state machines to coloured Petri nets using Acceleo: a report. In: Proceedings of the 3rd international workshop on engineering safety and security systems (ESSS 2014). EPTCS","DOI":"10.4204\/EPTCS.150.1"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/2237796.2237819"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Andr\u00e9 \u00c9 Choppy C Noulamo T (2014) Modelling timed concurrent systems using activity diagram patterns. In: Nguyen V-H Le A-C Huynh V-N (eds) Proceedings of the 6th international conference on knowledge and systems engineering (KSE\u201914) volume 326 of Advances in intelligent systems and computing. Springer pp 339-351","DOI":"10.1007\/978-3-319-11680-8_27"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Andr\u00e9 \u00c9 Choppy C Reggio G (2013) Activity diagrams patterns for modeling business processes. In: Lee R (ed) 11th international conference on software engineering research management and applications (SERA\u201913) volume 496 of Studies in computational intelligence. Springer pp 197\u2013213","DOI":"10.1007\/978-3-319-00948-3_13"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-002-0012-8"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Baresi L Pezz\u00e8 M (2001) On formalizing UML with high-level Petri nets. In: de Cindio GAF Rozenberg G (eds) Concurrent object-oriented programming and Petri nets. Advances in Petri nets volume 2001 of Lecture notes in computer science. Springer pp 276\u2013304","DOI":"10.1007\/3-540-45397-0_9"},{"issue":"7","key":"e_1_2_1_2_8_2","first-page":"597","article-title":"Capturing requirements by abstract state machines: the light control case study","volume":"6","author":"B\u00f6rger E","year":"2000","journal-title":"J Univ Comput Sci"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Berthomieu B Vernadat F (2006) Time Petri nets analysis with TINA. In: Proceedings of the third international conference on the quantitative evaluation of systems (QEST 2006) pp 123\u2013124. IEEE Computer Society","DOI":"10.1109\/QEST.2006.56"},{"key":"e_1_2_1_2_10_2","unstructured":"Carlsson M Johansson L (2009) Formal verification of UML-RT capsules using model checking. Master\u2019s thesis Department of Computer Science and Engineering Chalmers University of Technology. G\u00f6teborg Sweden"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/1921532.1921561"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Fecher H Sch\u00f6nborn J (2007) UML 2.0 state machines: complete formal semantics via core state machine. In: Proceedings of the 11th international workshop on formal methods: applications and technology (FMICS 2006) volume 4346 of Lecture notes in computer science. Springer pp 244\u2013260","DOI":"10.1007\/978-3-540-70952-7_16"},{"key":"e_1_2_1_2_13_2","unstructured":"Gerard S (2015) Papyrus UML Modeling tool 1.1.2. https:\/\/www.eclipse.org\/papyrus\/"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-8326(01)00012-1"},{"key":"e_1_2_1_2_15_2","unstructured":"Gogolla M Presicce FP (1998) State diagrams in UML: a formal semantics using graph transformations\u2014or diagrams are nice but graphs are worth their price. In: ICSE workshop on precise semantics of modelling techniques pp 55\u201372"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.596624"},{"key":"e_1_2_1_2_17_2","unstructured":"Holzmann GJ (2003) The SPIN model checker: primer and reference manual. Addison Wesley"},{"key":"e_1_2_1_2_18_2","unstructured":"Jussila T Dubrovin J Junttila T Latvala T Porres I (2006) Model checking dynamic and hierarchical UML state machines. In: MDV"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Jensen K Kristensen LM (2009) Coloured Petri nets\u2014modelling and validation of concurrent systems. Springer","DOI":"10.1007\/b95112"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Jacobs J Simpson A (2015) A formal model of SysML blocks using CSP for assured systems engineering. In: Proceedings of the 3rd international workshop on formal techniques for safety-critical systems (FTSCS 2014) volume 476 of Communications in computer and information science. Springer (To appear)","DOI":"10.1007\/978-3-319-17581-2_9"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Knapp A Merz S Rauh C (2002) Model checking\u2014timed UML state machines and collaborations. In: Formal techniques in real-time and fault-tolerant systems 7th International symposium FTRTFT volume 2469 of Lecture notes in computer science. Springer pp 395\u2013416","DOI":"10.1007\/3-540-45739-9_23"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"L\u00fcttgen G von der Beeck M Cleaveland R (1999) Statecharts via process algebra. In: 10th international conference on concurrency theory CONCUR volume 1664 of Lecture notes in computer science. Springer pp 399\u2013414","DOI":"10.1007\/3-540-48320-9_28"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11219-007-9020-9"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Liu S Liu Y Andr\u00e9 \u00c9 Choppy C Sun J Wadhwa B Dong JS (2013) A formal semantics for the complete syntax of UML state machines with communications. In: Proceedings of the 10th international conference on integrated formal methods (iFM\u201913) volume 7940 of Lecture notes in computer science. Springer pp 331\u2013346","DOI":"10.1007\/978-3-642-38613-8_23"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001659970003"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Lime D Roux OH Seidner C Traonouez L-M (2009) Romeo: a parametric model-checker for Petri nets with stopwatches. In: Kowalewski S Philippou A (eds) 15th International conference on tools and algorithms for the construction and analysis of systems (TACAS 2009) volume 5505 of LNCS. Springer pp 54\u201357","DOI":"10.1007\/978-3-642-00768-2_6"},{"key":"e_1_2_1_2_28_2","unstructured":"Merlin PM (1974) A study of the recoverability of computing systems. PhD thesis University of California Irvine CA USA"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Mekki A Ghazel M Toguyeni A (2009) Validating time-constrained systems using UML statecharts patterns and timed automata observers. In: VECoS pp 112\u2013124. British Computer Society","DOI":"10.14236\/ewic\/VECOS2009.11"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00381-4"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Ng MY Butler M (2002) Tool support for visualizing CSP in UML. In: Proceedings of the 4th international conference on formal engineering methods (ICFEM 2002) volume 2495 of Lecture notes in computer science. Springer pp 287\u2013298","DOI":"10.1007\/3-540-36103-0_31"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Ng MY Butler M (2003) Towards formalizing UML state diagrams in CSP. In: Proceedings of the 1st international conference on software engineering and formal methods (SEFM 2003) pp 138\u2013147. IEEE Computer Society","DOI":"10.1109\/SEFM.2003.1236215"},{"key":"e_1_2_1_2_33_2","unstructured":"OMG (2011) UML profile for MARTE: Modeling and Analysis of Real-Time and Embedded systems version 1.1. http:\/\/www.omg.org\/spec\/MARTE\/1.1\/PDF\/"},{"key":"e_1_2_1_2_34_2","unstructured":"OMG (2015) Unified Modeling Language (OMG UML) version 2.5. http:\/\/www.omg.org\/spec\/UML\/2.5\/"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Peron A (1995) Statecharts transition structures and transformations. In: Mosses PD Nielsen M Schwartzbach MI (eds) 6th International joint conference CAAP\/FASETAPSOFT\u201995: theory and practice of software development volume 915 of Lecture notes in computer science. Springer pp 454\u2013468","DOI":"10.1007\/3-540-59293-8_213"},{"key":"e_1_2_1_2_36_2","unstructured":"Pettit IV RG Gomaa H (2000) Validation of dynamic behavior in UML using colored Petri nets. In: Proceedings of UML\u20192000 workshop\u2014dynamic behaviour in UML models: semantic questions volume 1939 of Lecture notes in computer science. Springer Verlag pp 295\u2013302"},{"key":"e_1_2_1_2_37_2","unstructured":"Pettit IV RG Gomaa H (2001) Modeling state-dependent objects using colored Petri nets. In: Proceedings of workshop on modelling of objects components and agents pp 105\u2013120"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Pettit IV RG Gomaa H (2006) Modeling behavioral patterns of concurrent objects using Petri nets. In: 9th IEEE international symposium on object-oriented real-time distributed computing ISORC pp 303\u2013312. IEEE Computer Society","DOI":"10.1109\/ISORC.2006.55"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","DOI":"10.1016\/B978-0-7506-8706-5.00002-7","volume-title":"A crash course in UML state machines","author":"Samek M","year":"2009"},{"key":"e_1_2_1_2_40_2","unstructured":"Sch\u00f6nborn J (2005) Formal semantics of UML 2.0 behavioral state machines. Technical report Institute of Computer Science and Applied Mathematics Christian-Albrechts-University of Kiel"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Sun J Liu Y Dong JS Pang J (2009) PAT: towards flexible verification under fairness. In: Proceedings of the 21st international conference on computer aided verification (CAV 2009) volume 5643 of Lecture notes in computer science. Springer","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-008-0065-0"},{"issue":"17","key":"e_1_2_1_2_43_2","first-page":"3273","article-title":"Parametric model-checking of stopwatch Petri nets","volume":"15","author":"Traonouez L-M","year":"2009","journal-title":"J Univ Comput Sci"},{"key":"e_1_2_1_2_44_2","unstructured":"Trowitzsch J Zimmermann A (2005) Real-time UML state machines: an analysis approach. In: Workshop on object oriented software design for real time and embedded computer systems (Net.ObjectDays 2005)"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Westergaard M (2013) CPN Tools 4: multi-formalism and extensibility. In: Proceedings of the 34th international conference on application and theory of Petri nets and concurrency (Petri Nets 2013) volume 7927 of Lecture notes in computer science. Springer pp 400\u2013409","DOI":"10.1007\/978-3-642-38697-8_22"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Zhang S Liu Y (2010) An automatic approach to model checking UML state machines. In: SSIRI-C pp 1\u20136. IEEE","DOI":"10.1109\/SSIRI-C.2010.11"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0388-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0388-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0388-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T17:31:30Z","timestamp":1749058290000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0388-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9]]},"references-count":46,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2016,9]]}},"alternative-id":["10.1007\/s00165-016-0388-9"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0388-9","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,9]]}}}