{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,25]],"date-time":"2025-07-25T10:24:03Z","timestamp":1753439043300,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":38,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,10,14]],"date-time":"2018-10-14T00:00:00Z","timestamp":1539475200000},"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":[],"published-print":{"date-parts":[[2018,10,14]]},"DOI":"10.1145\/3239372.3239395","type":"proceedings-article","created":{"date-parts":[[2018,10,4]],"date-time":"2018-10-04T12:21:55Z","timestamp":1538655715000},"page":"112-122","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Unified LTL Verification and Embedded Execution of UML Models"],"prefix":"10.1145","author":[{"given":"Valentin","family":"Besnard","sequence":"first","affiliation":[{"name":"ERIS, ESEO-TECH, Angers, France"}]},{"given":"Matthias","family":"Brun","sequence":"additional","affiliation":[{"name":"ERIS, ESEO-TECH, Angers, France"}]},{"given":"Fr\u00e9d\u00e9ric","family":"Jouault","sequence":"additional","affiliation":[{"name":"ERIS, ESEO-TECH, Angers, France"}]},{"given":"Ciprian","family":"Teodorov","sequence":"additional","affiliation":[{"name":"Lab-STICC UMR CNRS 6285, ENSTA Bretagne, Brest, France"}]},{"given":"Philippe","family":"Dhaussy","sequence":"additional","affiliation":[{"name":"Lab-STICC UMR CNRS 6285, ENSTA Bretagne, Brest, France"}]}],"member":"320","published-online":{"date-parts":[[2018,10,14]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_3_2_1_1_1","DOI":"10.1145\/1289927.1289967"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_2_1","DOI":"10.1007\/978-3-642-28756-5_8"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_3_1","DOI":"10.1145\/3106237.3106278"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_4_1","DOI":"10.1109\/RTAS.2006.7"},{"key":"e_1_3_2_1_5_1","volume-title":"3rd International Workshop on Executable Modeling (EXE","author":"Besnard Valentin","year":"2017","unstructured":"Valentin Besnard , Matthias Brun , Philippe Dhaussy , Fr\u00e9d\u00e9ric Jouault , David Olivier , and Ciprian Teodorov . 2017 . Towards one Model Interpreter for Both Design and Deployment . In 3rd International Workshop on Executable Modeling (EXE 2017). Austin, United States. Valentin Besnard, Matthias Brun, Philippe Dhaussy, Fr\u00e9d\u00e9ric Jouault, David Olivier, and Ciprian Teodorov. 2017. Towards one Model Interpreter for Both Design and Deployment. In 3rd International Workshop on Executable Modeling (EXE 2017). Austin, United States."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_6_1","DOI":"10.1145\/2814251.2814262"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_7_1","DOI":"10.1145\/2997364.2997384"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_8_1","DOI":"10.1109\/SENSORCOMM.2009.27"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_9_1","DOI":"10.1109\/ISORC.2012.30"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_11_1","DOI":"10.1145\/3183399.3183406"},{"key":"e_1_3_2_1_12_1","volume-title":"Execution of UML models: a systematic review of research and practice. Software & Systems Modeling (10","author":"Ciccozzi Federico","year":"2018","unstructured":"Federico Ciccozzi , Ivano Malavolta , and Bran Selic . 2018. Execution of UML models: a systematic review of research and practice. Software & Systems Modeling (10 Apr 2018 ). Federico Ciccozzi, Ivano Malavolta, and Bran Selic. 2018. Execution of UML models: a systematic review of research and practice. Software & Systems Modeling (10 Apr 2018)."},{"key":"e_1_3_2_1_13_1","volume-title":"Jo\u00ebl Champeau, Benoit Combemale, and Ciprian Teodorov.","author":"Deantoni Julien","year":"2014","unstructured":"Julien Deantoni , Papa Issa Diallo , Jo\u00ebl Champeau, Benoit Combemale, and Ciprian Teodorov. 2014 . Operational Semantics of the Model of Concurrency and Communication Language . Research Report RR-8584. INRIA. 23 pages. Julien Deantoni, Papa Issa Diallo, Jo\u00ebl Champeau, Benoit Combemale, and Ciprian Teodorov. 2014. Operational Semantics of the Model of Concurrency and Communication Language. Research Report RR-8584. INRIA. 23 pages."},{"key":"e_1_3_2_1_14_1","volume-title":"Comparison of Algorithms for Checking Emptiness on B\u00fcchi Automata. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)","volume":"13","author":"Gaiser Andreas","year":"2009","unstructured":"Andreas Gaiser and Stefan Schwoon . 2009 . Comparison of Algorithms for Checking Emptiness on B\u00fcchi Automata. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09) (OpenAccess Series in Informatics (OASIcs)), Petr Hlinen\u00fd, V\u00e1clav Maty\u00e1\u0161, and Tom\u00e1\u0161 Vojnar (Eds.) , Vol. 13 . Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 18--26. Andreas Gaiser and Stefan Schwoon. 2009. Comparison of Algorithms for Checking Emptiness on B\u00fcchi Automata. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09) (OpenAccess Series in Informatics (OASIcs)), Petr Hlinen\u00fd, V\u00e1clav Maty\u00e1\u0161, and Tom\u00e1\u0161 Vojnar (Eds.), Vol. 13. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 18--26."},{"key":"e_1_3_2_1_15_1","volume-title":"Rhapsody: A Complete Life-Cycle Model-Based Development System","author":"Gery Eran","year":"2002","unstructured":"Eran Gery , David Harel , and Eldad Palachi . 2002 . Rhapsody: A Complete Life-Cycle Model-Based Development System . In Integrated Formal Methods, Michael Butler, Luigia Petre, and Kaisa Sere (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 1--10. Eran Gery, David Harel, and Eldad Palachi. 2002. Rhapsody: A Complete Life-Cycle Model-Based Development System. In Integrated Formal Methods, Michael Butler, Luigia Petre, and Kaisa Sere (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1--10."},{"unstructured":"Ian Wilkie Adrian King Mike Clarke Chas Weaver Chris Raistrick and Paul Francis. 2003. UML ASL Reference Guide. http:\/\/www.ooatool.com\/docs\/ASL03.pdf Kennedy Carter.  Ian Wilkie Adrian King Mike Clarke Chas Weaver Chris Raistrick and Paul Francis. 2003. UML ASL Reference Guide. http:\/\/www.ooatool.com\/docs\/ASL03.pdf Kennedy Carter.","key":"e_1_3_2_1_16_1"},{"unstructured":"Galois Inc. {n. d.}. The Haskell Lightweight Virtual Machine (HaLVM): GHC running on Xen. https:\/\/github.com\/GaloisInc\/HaLVM  Galois Inc. {n. d.}. The Haskell Lightweight Virtual Machine (HaLVM): GHC running on Xen. https:\/\/github.com\/GaloisInc\/HaLVM","key":"e_1_3_2_1_17_1"},{"unstructured":"Project Technology Inc. 2008. Object Action Language Reference Manual. http:\/\/www.ooatool.com\/docs\/OAL08.pdf  Project Technology Inc. 2008. Object Action Language Reference Manual. http:\/\/www.ooatool.com\/docs\/OAL08.pdf","key":"e_1_3_2_1_18_1"},{"volume-title":"Model-Based Debugging of Embedded Software Systems","author":"Iyenghar Padma","unstructured":"Padma Iyenghar , Elke Pulvermueller , Clemens Westerkamp , Juergen Wuebbelmann , and Michael Uelschen . 2017. Model-Based Debugging of Embedded Software Systems . Springer New York , New York, NY , 107--132. Padma Iyenghar, Elke Pulvermueller, Clemens Westerkamp, Juergen Wuebbelmann, and Michael Uelschen. 2017. Model-Based Debugging of Embedded Software Systems. Springer New York, New York, NY, 107--132.","key":"e_1_3_2_1_19_1"},{"key":"e_1_3_2_1_20_1","volume-title":"Luka Le Roux, and Philippe Dhaussy","author":"Jouault Fr\u00e9d\u00e9ric","year":"2014","unstructured":"Fr\u00e9d\u00e9ric Jouault , Ciprian Teodorov , J\u00e9r\u00f4me Delatour , Luka Le Roux, and Philippe Dhaussy . 2014 . Transformation de mod\u00e8les UML vers Fiacre, via les langages interm\u00e9diaires tUML et ABCD. G\u00e9nie logiciel 109 (June 2014). Fr\u00e9d\u00e9ric Jouault, Ciprian Teodorov, J\u00e9r\u00f4me Delatour, Luka Le Roux, and Philippe Dhaussy. 2014. Transformation de mod\u00e8les UML vers Fiacre, via les langages interm\u00e9diaires tUML et ABCD. G\u00e9nie logiciel 109 (June 2014)."},{"key":"e_1_3_2_1_21_1","volume-title":"Proceedings of the Fifth European Conference on Model-Driven Architecture Foundations and Applications (ECMDAFA","author":"Lanusse Agnes","year":"2009","unstructured":"Agnes Lanusse , Yann Tanguy , Huascar Espinoza , Chokri Mraidha , Sebastien Gerard , Patrick Tessier , Remi Schnekenburger , Hubert Dubois , and Fran\u00e7ois Terrier . 2009 . Papyrus UML: an open source toolset for MDA . In Proceedings of the Fifth European Conference on Model-Driven Architecture Foundations and Applications (ECMDAFA 2009). 1--4. Agnes Lanusse, Yann Tanguy, Huascar Espinoza, Chokri Mraidha, Sebastien Gerard, Patrick Tessier, Remi Schnekenburger, Hubert Dubois, and Fran\u00e7ois Terrier. 2009. Papyrus UML: an open source toolset for MDA. In Proceedings of the Fifth European Conference on Model-Driven Architecture Foundations and Applications (ECMDAFA 2009). 1--4."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_22_1","DOI":"10.1147\/sj.453.0555"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_23_1","DOI":"10.1145\/605432.605407"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_24_1","DOI":"10.1145\/2448076.2448079"},{"volume-title":"xMOF: Executable DSMLs Based on fUML","author":"Mayerhofer Tanja","unstructured":"Tanja Mayerhofer , Philip Langer , Manuel Wimmer , and Gerti Kappel . 2013. xMOF: Executable DSMLs Based on fUML . In Software Language Engineering, Martin Erwig, Richard F. Paige, and Eric Van Wyk (Eds.). Springer International Publishing , Cham , 56--75. Tanja Mayerhofer, Philip Langer, Manuel Wimmer, and Gerti Kappel. 2013. xMOF: Executable DSMLs Based on fUML. In Software Language Engineering, Martin Erwig, Richard F. Paige, and Eric Van Wyk (Eds.). Springer International Publishing, Cham, 56--75.","key":"e_1_3_2_1_25_1"},{"unstructured":"M Mohlin. 2011. Using the UML Action Language in Rational Software Architect.  M Mohlin. 2011. Using the UML Action Language in Rational Software Architect.","key":"e_1_3_2_1_26_1"},{"unstructured":"OMG. 2017. Action Language for Foundational UML (Alf). www.omg.org\/spec\/ALF\/1.1\/PDF  OMG. 2017. Action Language for Foundational UML (Alf). www.omg.org\/spec\/ALF\/1.1\/PDF","key":"e_1_3_2_1_27_1"},{"unstructured":"OMG. 2017. Semantics of a Foundational Subset for Executable UML Models. https:\/\/www.omg.org\/spec\/FUML\/1.3\/PDF  OMG. 2017. Semantics of a Foundational Subset for Executable UML Models. https:\/\/www.omg.org\/spec\/FUML\/1.3\/PDF","key":"e_1_3_2_1_28_1"},{"unstructured":"OMG. 2017. Unified Modeling Language. https:\/\/www.omg.org\/spec\/UML\/2.5.1\/PDF  OMG. 2017. Unified Modeling Language. https:\/\/www.omg.org\/spec\/UML\/2.5.1\/PDF","key":"e_1_3_2_1_29_1"},{"volume-title":"Formal Methods for Railway Operation and Control Systems (Proceedings of the FORMS-2003 Conference)","author":"Pint\u00e9r Gergely","unstructured":"Gergely Pint\u00e9r and Istv\u00e1n Majzik . 2003. Automatic Code Generation Based on Formally Analyzed UML Statechart Models . In Formal Methods for Railway Operation and Control Systems (Proceedings of the FORMS-2003 Conference) , G. Tarnai and E. Schnieder (Eds.). L'Harmattan, Budapest, Hungary , 45--52. Gergely Pint\u00e9r and Istv\u00e1n Majzik. 2003. Automatic Code Generation Based on Formally Analyzed UML Statechart Models. In Formal Methods for Railway Operation and Control Systems (Proceedings of the FORMS-2003 Conference), G. Tarnai and E. Schnieder (Eds.). L'Harmattan, Budapest, Hungary, 45--52.","key":"e_1_3_2_1_30_1"},{"key":"e_1_3_2_1_31_1","first-page":"3","article-title":"Program Code Generation based on UML Statechart Models","volume":"47","author":"Pint\u00e9r Gergely","year":"2003","unstructured":"Gergely Pint\u00e9r and Istv\u00e1n Majzik . 2003 . Program Code Generation based on UML Statechart Models . Periodica Polytechnica 47 , 3 - 4 (2003), 187--204. Gergely Pint\u00e9r and Istv\u00e1n Majzik. 2003. Program Code Generation based on UML Statechart Models. Periodica Polytechnica 47, 3-4 (2003), 187--204.","journal-title":"Periodica Polytechnica"},{"key":"e_1_3_2_1_32_1","volume-title":"Proceedings of Synchronous Languages, Applications, and Programming (SLAP), International Workshop on Synchronous Languages, Applications, and Programming (SLAP'06)","volume":"126","author":"Plummer Becky","unstructured":"Becky Plummer , Mukul Khajanchi , and Stephen A. Edwards . 2006. An Esterel Virtual Machine for Embedded Systems . In Proceedings of Synchronous Languages, Applications, and Programming (SLAP), International Workshop on Synchronous Languages, Applications, and Programming (SLAP'06) (Ed.), Vol. 126 . Vienna, Austria, 912--917. Becky Plummer, Mukul Khajanchi, and Stephen A. Edwards. 2006. An Esterel Virtual Machine for Embedded Systems. In Proceedings of Synchronous Languages, Applications, and Programming (SLAP), International Workshop on Synchronous Languages, Applications, and Programming (SLAP'06) (Ed.), Vol. 126. Vienna, Austria, 912--917."},{"key":"e_1_3_2_1_33_1","volume-title":"Papyrus: Moka Overview. https:\/\/wiki.eclipse.org\/Papyrus\/UserGuide\/ModelExecution","author":"Revol Sebastien","year":"2018","unstructured":"Sebastien Revol , G\u00e9ry Delog , Arnaud Cuccurru , and J\u00e9r\u00e9mie Tatibou\u00ebt . 2018 . Papyrus: Moka Overview. https:\/\/wiki.eclipse.org\/Papyrus\/UserGuide\/ModelExecution Sebastien Revol, G\u00e9ry Delog, Arnaud Cuccurru, and J\u00e9r\u00e9mie Tatibou\u00ebt. 2018. Papyrus: Moka Overview. https:\/\/wiki.eclipse.org\/Papyrus\/UserGuide\/ModelExecution"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_34_1","DOI":"10.1109\/VLHCC.2005.64"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_35_1","DOI":"10.1145\/1094855.1094908"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_36_1","DOI":"10.1007\/s10009-015-0401-2"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_37_1","DOI":"10.1002\/stvr.1611"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_38_1","DOI":"10.1109\/MODELS.2015.7338249"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_39_1","DOI":"10.1145\/2384716.2384767"}],"event":{"sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"],"acronym":"MODELS '18","name":"MODELS '18: ACM\/IEEE 21th International Conference on Model Driven Engineering Languages and Systems","location":"Copenhagen Denmark"},"container-title":["Proceedings of the 21th ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3239372.3239395","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3239372.3239395","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:08:19Z","timestamp":1750208899000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3239372.3239395"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,14]]},"references-count":38,"alternative-id":["10.1145\/3239372.3239395","10.1145\/3239372"],"URL":"https:\/\/doi.org\/10.1145\/3239372.3239395","relation":{},"subject":[],"published":{"date-parts":[[2018,10,14]]},"assertion":[{"value":"2018-10-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}