{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,23]],"date-time":"2026-06-23T08:07:48Z","timestamp":1782202068431,"version":"3.54.5"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2024,8,14]],"date-time":"2024-08-14T00:00:00Z","timestamp":1723593600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2024,9,30]]},"abstract":"<jats:p>Although Unified Modeling Language (UML) state machines constitute a convenient modeling formalism that is widely used in many applications, the lack of formal semantics impedes carrying out automatic processing, such as formal verification. In this article, we aim to achieve a proven translation from a subset of UML state machines to timed automata. A generic abstract syntax is defined for state machines that allows us to specify state machines as a tree-like structure, explicitly illustrating the hierarchical relationships within the model. Based on this syntax, a formal asynchronous semantics for state machines and systems of state machines is established. Additionally, the semantics of timed automata is specified. Then, a translation relation from the considered set of state machines to timed automata is defined and a strong equivalence relation \u2014 namely, a timed bisimulation between the source and target models \u2014 is formally proven. The proof is carried out inductively while considering continuous (time) and discrete transitions separately. This proof allows us to demonstrate a strong similitude between these models.<\/jats:p>","DOI":"10.1145\/3581771","type":"journal-article","created":{"date-parts":[[2023,1,25]],"date-time":"2023-01-25T11:55:19Z","timestamp":1674647719000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["A Proven Translation from a UML State Machine Subset to Timed Automata"],"prefix":"10.1145","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3998-2948","authenticated-orcid":false,"given":"Florent","family":"Peres","sequence":"first","affiliation":[{"name":"Universit\u00e9 Gustave Eiffel, COSYS-ESTAS, Villeneuve d'Ascq, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1160-7997","authenticated-orcid":false,"given":"Mohamed","family":"Ghazel","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Gustave Eiffel, COSYS-ESTAS, Villeneuve d'Ascq, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,8,14]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","unstructured":"Rajeev Alur and David L. Dill. 1994. A theory of timed automata. Theoretical Computer Science 126 2 (April1994) 183\u2013235. 10.1016\/0304-3975(94)90010-8","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_2_3_2","unstructured":"Tobias Amnell Alexandre David Elena Fersman M. Moller and Paul Petterson. 2001. Tools for real-time UML: Formal verification and code synthesis. (Sept.2001)."},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75209-7_38"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/11430230_9"},{"key":"e_1_3_2_6_2","doi-asserted-by":"crossref","unstructured":"Bernard Berthomieu Florent Peres and Fran\u00e7ois Vernadat. 2006. Bridging the gap between timed automata and bounded time petri nets. In Formal Modeling and Analysis of Timed Systems: 4th International Conference (FORMATS\u201906). Springer Berlin Heidelberg 82\u201397.","DOI":"10.1007\/11867340_7"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Egon B\u00f6rger Alessandra Cavarra and Elvinia Riccobene. 2004. On formalizing UML state machines using ASMs. Information and Software Technology 46 5 (April2004) 287\u2013292. 10.1016\/j.infsof.2003.09.009","DOI":"10.1016\/j.infsof.2003.09.009"},{"key":"e_1_3_2_8_2","doi-asserted-by":"crossref","unstructured":"Franck Cassez and Olivier Henri Roux. 2006. Structural translation from time petri nets to timed automata. Journal of Systems and Software 29 1 (2006) 1456\u20131468. https:\/\/hal.archives-ouvertes.fr\/hal-00139236. Publisher: Elsevier.","DOI":"10.1016\/j.jss.2005.12.021"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/11557432_8"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","unstructured":"Werner Damm Bernhard Josko Amir Pnueli and Anjelika Votintseva. 2005. A discrete-time UML semantics for concurrency and communication in safety-critical applications. Science of Computer Programming 55 (March2005) 81\u2013115. 10.1016\/j.scico.2004.05.012","DOI":"10.1016\/j.scico.2004.05.012"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"Alexandre David and M. Oliver M\u00f6ller. 2001. From HUPPAAL to UPPAAL - A translation from hierarchical timed automata to flat timed automata. BRICS Report Series11 (March2001). 10.7146\/brics.v8i11.20467. Number: 11.","DOI":"10.7146\/brics.v8i11.20467"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.5555\/827268.828974"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","unstructured":"Salvatore Distefano Marco Scarpa and Antonio Puliafito. 2011. From UML to petri nets: The PCM-based methodology. IEEE Transactions on Software Engineering 37 1 (March2011) 65\u201379. 10.1109\/TSE.2010.10","DOI":"10.1109\/TSE.2010.10"},{"key":"e_1_3_2_14_2","volume-title":"Doing Hard Time: Developing Real-Time Systems with UML, Objects, Frameworks, and Patterns (1st ed.)","author":"Douglass Bruce Powel","year":"1999","unstructured":"Bruce Powel Douglass. 1999. Doing Hard Time: Developing Real-Time Systems with UML, Objects, Frameworks, and Patterns (1st ed.). Addison Wesley, Boston."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35520-7_6"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/11576280_5"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"Mohamed Ghazel. 2014. Formalizing a subset of ERTMS\/ETCS specifications for verification purposes. Transportation Research Part C: Emerging Technologies 42 (May2014) 60\u201375. 10.1016\/j.trc.2014.02.002","DOI":"10.1016\/j.trc.2014.02.002"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","unstructured":"Mohamed Ghazel Armand Toguy\u00e9ni and Michel Bigand. 2004. An UML approach for the metamodelling of automated production systems for monitoring purpose. Computers in Industry 55 3 (Dec.2004) 283\u2013299. 10.1016\/j.compind.2004.08.005","DOI":"10.1016\/j.compind.2004.08.005"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","unstructured":"David Harel and Amnon Naamad. 1996. The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology 5 4 (Oct.1996) 293\u2013333. 10.1145\/235321.235322","DOI":"10.1145\/235321.235322"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","unstructured":"T. A. Henzinger X. Nicollin J. Sifakis and S. Yovine. 1994. Symbolic model checking for real-time systems. Information and Computation 111 2 (June1994) 193\u2013244. 10.1006\/inco.1994.1045","DOI":"10.1006\/inco.1994.1045"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.5555\/3019255"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45739-9_23"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69814-2_6"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_24"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2005.49"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"Ruggero Lanotte Andrea Maggiolo-Schettini and Angelo Troina. 2010. Reachability results for timed automata with unbounded data structures. Acta Informatica 47 (Sept.2010) 279\u2013311. 10.1007\/s00236-010-0121-8","DOI":"10.1007\/s00236-010-0121-8"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Kim G. Larsen Paul Pettersson and Wang Yi. 1997. UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer 1 1-2 (Dec.1997) 134\u2013152. 10.1007\/s100090050010","DOI":"10.1007\/s100090050010"},{"key":"e_1_3_2_28_2","doi-asserted-by":"crossref","unstructured":"Shuang Liu Yang Liu \u00c9tienne Andr\u00e9 Christine Choppy Jun Sun Bimlesh Wadhwa and Jin Song Dong. 2013. A formal semantics for complete UML state machines with communications. In International Conference on Integrated Formal Methods (IFM\u201913) Einar Broch Johnsen and Luigia Petre (Eds.). Lecture Notes in Computer Science Springer Berlin 331\u2013346.","DOI":"10.1007\/978-3-642-38613-8_23"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","unstructured":"Chuan Ma and W. M. Wonham. 2006. Nonblocking supervisory control of state tree structures. IEEE Transactions on Automatic Control 51 5 (May2006) 782\u2013793. 10.1109\/TAC.2006.875030","DOI":"10.1109\/TAC.2006.875030"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","unstructured":"Ivano Malavolta Henry Muccini Patrizio Pelliccione and Damien Tamburri. 2010. Providing architectural languages and tools interoperability through model transformation technologies. IEEE Transactions on Software Engineering 36 1 (Jan.2010) 119\u2013140. 10.1109\/TSE.2009.51. Conference Name: IEEE Transactions on Software Engineering.","DOI":"10.1109\/TSE.2009.51"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"Fr\u00e9d\u00e9ric Mallet. 2008. CCSL: Specifying clock constraints with UML\/MARTE. Innovations in Systems and Software Engineering 4 3 (2008) 309. 10.1007\/s11334-008-0055-2","DOI":"10.1007\/s11334-008-0055-2"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","unstructured":"Ahmed Mekki Mohamed Ghazel and Armand Toguyeni. 2009. Validating time-constrained systems using UML statecharts patterns and timed automata observers. (July2009). BCS Learning & Development. 10.14236\/ewic\/VECOS2009.11","DOI":"10.14236\/ewic\/VECOS2009.11"},{"key":"e_1_3_2_33_2","unstructured":"Philip Meir Merlin. 1974. A study of the recoverability of computing systems. (Nov.1974). https:\/\/escholarship.org\/uc\/item\/1p80c4fg."},{"key":"e_1_3_2_34_2","volume-title":"UML-B Specification for Proven Embedded Systems Design","unstructured":"Fredrik Bernin, et\u00a0al. 2004. UML-B Specification for Proven Embedded Systems Design. Springer."},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","unstructured":"Ariadi Nugroho. 2009. Level of detail in UML models and its impact on model comprehension: A controlled experiment. Information and Software Technology 51 12 (Dec.2009) 1670\u20131685. 10.1016\/j.infsof.2009.04.007","DOI":"10.1016\/j.infsof.2009.04.007"},{"key":"e_1_3_2_36_2","unstructured":"OMG. 2017. About the Unified Modeling Language Specification Version 2.5.1. Retrieved February 10 2023 from https:\/\/www.omg.org\/spec\/UML\/2.5.1\/About-UML."},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"Florent Peres Bernard Berthomieu and Fran\u00e7ois Vernadat. 2011. On the composition of time Petri nets. Discrete Event Dynamic Systems 21 3 (April2011) 395. 10.1007\/s10626-011-0102-2","DOI":"10.1007\/s10626-011-0102-2"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","unstructured":"Anna Queralt and Ernest Teniente. 2012. Verification and validation of UML conceptual schemas with OCL constraints. ACM Transactions on Software Engineering and Methodology 21 2 (March2012) 13:1\u201313:41. 10.1145\/2089116.2089123","DOI":"10.1145\/2089116.2089123"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","unstructured":"Jun Sun Yang Liu Jin Song Dong Yan Liu Ling Shi and \u00c9tienne Andr\u00e9. 2013. Modeling and verifying hierarchical real-time systems using stateful timed CSP. ACM Transactions on Software Engineering and Methodology 22 1 (March2013) 3:1\u20133:29. 10.1145\/2430536.2430537","DOI":"10.1145\/2430536.2430537"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","unstructured":"Hee Beng Kuan Tan Yong Yang and Lei Bian. 2006. Systematic transformation of functional analysis model into OO design and implementation. IEEE Transactions on Software Engineering 32 02 (Feb.2006) 111\u2013135. 10.1109\/TSE.2006.20Publisher: IEEE Computer Society.","DOI":"10.1109\/TSE.2006.20"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3581771","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3581771","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:38Z","timestamp":1750183718000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3581771"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,14]]},"references-count":39,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2024,9,30]]}},"alternative-id":["10.1145\/3581771"],"URL":"https:\/\/doi.org\/10.1145\/3581771","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,8,14]]},"assertion":[{"value":"2022-01-17","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-11-23","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-14","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}