{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T02:19:37Z","timestamp":1783477177843,"version":"3.55.0"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2024,6,25]],"date-time":"2024-06-25T00:00:00Z","timestamp":1719273600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,6,25]],"date-time":"2024-06-25T00:00:00Z","timestamp":1719273600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002957","name":"Technische Universit\u00e4t Dresden","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100002957","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2024,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Verifying industrial robotic systems is a complex task because those systems are distributed and solely defined by their implementation instead of models of the system to be verified. Some technologies mitigate parts of this problem, e.g., robotic middleware such as the Robotic Operating System (ROS) or concrete solutions such as automata-based specification of robot behavior. However, they all lack the required modeling depth to describe the structure, behavior, and communication of the system. We introduce an improved version of our previous model-driven approach based on Petri nets, integrating these three aspects of ROS-based systems. Using a formal modeling language enables verification of the described system and the generation of complete system parts in the form of ROS nodes. This reduces testing effort because the specification of component workflows and interfaces remains formally proven, while only changed implementations have to be revalidated. We extended our previous approach with novel model transformations, which considerably improved our approach\u2019s performance and memory requirements. We evaluate our approach in a case study involving multiple industrial robotic arms and show that the structure of and communication between ROS nodes can be described and verified.<\/jats:p>","DOI":"10.1007\/s11334-024-00570-5","type":"journal-article","created":{"date-parts":[[2024,6,25]],"date-time":"2024-06-25T19:16:03Z","timestamp":1719342963000},"page":"531-557","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Distributed Petri nets for model-driven verifiable robotic applications in ROS"],"prefix":"10.1007","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6504-9233","authenticated-orcid":false,"given":"Sebastian","family":"Ebert","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5778-4019","authenticated-orcid":false,"given":"Johannes","family":"Mey","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3247-0264","authenticated-orcid":false,"given":"Ren\u00e9","family":"Sch\u00f6ne","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1537-7815","authenticated-orcid":false,"given":"Sebastian","family":"G\u00f6tz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3513-6448","authenticated-orcid":false,"given":"Uwe","family":"A\u00dfmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,6,25]]},"reference":[{"key":"570_CR1","doi-asserted-by":"crossref","unstructured":"Ciccozzi F, Di\u00a0Ruscio D, Malavolta I, Pelliccione P, Tumova J (2017) Engineering the software of robotic systems. In: 2017 IEEE\/ACM 39th International conference on software engineering companion (ICSE-C), pp 507\u2013508. IEEE","DOI":"10.1109\/ICSE-C.2017.167"},{"key":"570_CR2","unstructured":"Quigley M, Conley K, Gerkey B, Faust J, Foote T, Leibs J et al (2009) ROS: an open-source Robot Operating System. In: ICRA Workshop on open source software, vol 3, p 5. Kobe, Japan"},{"key":"570_CR3","doi-asserted-by":"publisher","unstructured":"Lesire C, Pommereau F (2018) ASPiC: an acting system based on skill petri net composition. In: International conference on intelligent robots and systems (IROS), pp. 6952\u20136958. https:\/\/doi.org\/10.1109\/IROS.2018.8594328 . IEEE","DOI":"10.1109\/IROS.2018.8594328"},{"key":"570_CR4","doi-asserted-by":"publisher","unstructured":"Dondrup C, Papaioannou I, Lemon O (2019) Petri Net machines for human-agent interaction . https:\/\/doi.org\/10.48550\/arXiv.1909.06174","DOI":"10.48550\/arXiv.1909.06174"},{"key":"570_CR5","doi-asserted-by":"crossref","unstructured":"Pelletier B, Lesire C, Grand C, Doose D, Rognant M (2023) Predictive runtime verification of skill-based robotic systems using Petri Nets. In: 2023 IEEE International conference on robotics and automation (ICRA), pp 10580\u201310586. IEEE","DOI":"10.1109\/ICRA48891.2023.10160434"},{"key":"570_CR6","unstructured":"Santos PMP (2016) PN-RTE, petri net robot task execution. Master\u2019s thesis, Tecnico Lisboa"},{"issue":"2","key":"570_CR7","doi-asserted-by":"publisher","first-page":"688","DOI":"10.1109\/LRA.2022.3229231","volume":"8","author":"M Figat","year":"2022","unstructured":"Figat M, Zieli\u0144ski C (2022) Synthesis of robotic system controllers using robotic system specification language. IEEE Robot Autom Lett 8(2):688\u2013695","journal-title":"IEEE Robot Autom Lett"},{"key":"570_CR8","doi-asserted-by":"publisher","first-page":"104301","DOI":"10.1016\/j.robot.2022.104301","volume":"159","author":"S Dal Zilio","year":"2023","unstructured":"Dal Zilio S, Hladik P-E, Ingrand F, Mallet A (2023) A formal toolchain for offline and run-time verification of robotic systems. Robot Auton Syst 159:104301","journal-title":"Robot Auton Syst"},{"key":"570_CR9","doi-asserted-by":"publisher","unstructured":"Halder R, Proen\u00e7a J, Macedo N, Santos A (2017) Formal verification of ROS-based robotic applications using timed-automata. In: 2017 IEEE\/ACM 5th International FME workshop on formal methods in software engineering (FormaliSE). https:\/\/doi.org\/10.1109\/FormaliSE.2017.9. IEEE","DOI":"10.1109\/FormaliSE.2017.9"},{"issue":"1","key":"570_CR10","doi-asserted-by":"publisher","first-page":"1096","DOI":"10.1109\/JSYST.2018.2867285","volume":"13","author":"R Wang","year":"2018","unstructured":"Wang R, Guan Y, Song H, Li X, Li X, Shi Z, Song X (2018) A formal model-based design method for robotic systems. IEEE Syst J 13(1):1096\u20131107. https:\/\/doi.org\/10.1109\/JSYST.2018.2867285","journal-title":"IEEE Syst J"},{"key":"570_CR11","doi-asserted-by":"publisher","unstructured":"Cheng BH, Clark RJ, Fleck JE, Langford MA, et al.: (2020) AC-ROS: assurance case driven adaptation for the robot operating system. In: Proceedings of the 23rd ACM\/IEEE international conference on model driven engineering languages and systems. https:\/\/doi.org\/10.1145\/3365438.3410952","DOI":"10.1145\/3365438.3410952"},{"key":"570_CR12","doi-asserted-by":"publisher","unstructured":"Kortik S, Shastha TK (2021) Formal verification of ROS based systems using a linear logic theorem prover. In: International conference on robotics and automation (ICRA), pp 9368\u20139374. https:\/\/doi.org\/10.1109\/ICRA48506.2021.9561191. IEEE","DOI":"10.1109\/ICRA48506.2021.9561191"},{"key":"570_CR13","doi-asserted-by":"publisher","unstructured":"Zander S, Heppner G, Neugschwandtner G, Awad R, Essinger M, Ahmed N (2015) A model-driven engineering approach for ROS using ontological semantics. In: 6th International workshop on domain-specific languages and models for robotic systems (DSLRob-15). https:\/\/doi.org\/10.48550\/arXiv.1601.03998","DOI":"10.48550\/arXiv.1601.03998"},{"key":"570_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/s00170-018-1976-z","author":"E Est\u00e9vez","year":"2018","unstructured":"Est\u00e9vez E, Garc\u00eda A, Garc\u00eda J, Ortega J (2018) ART$$^2$$ool: a model-driven framework to generate target code for robot handling tasks. Int J Adv Manuf Technol. https:\/\/doi.org\/10.1007\/s00170-018-1976-z","journal-title":"Int J Adv Manuf Technol"},{"key":"570_CR15","doi-asserted-by":"publisher","unstructured":"Chaudhuri SR, Banerjee A, Swaminathan N, Choppella V, Pal A, Balamurali P (2019) A knowledge centric approach to conceptualizing robotic solutions. In: Proceedings of the 12th innovations on software engineering conference, pp 1\u201311 . https:\/\/doi.org\/10.1145\/3299771.3299782","DOI":"10.1145\/3299771.3299782"},{"key":"570_CR16","doi-asserted-by":"publisher","unstructured":"Kilgo P, Syriani E, Anderson M (2012) A visual modeling language for RDIS and ROS nodes using AToM 3. Lecture notes in computer science 7628 LNAI, 125\u2013136 https:\/\/doi.org\/10.1007\/978-3-642-34327-8_14","DOI":"10.1007\/978-3-642-34327-8_14"},{"issue":"2","key":"570_CR17","doi-asserted-by":"publisher","first-page":"1404","DOI":"10.1109\/JSYST.2016.2583403","volume":"12","author":"A Beaulieu","year":"2018","unstructured":"Beaulieu A, Givigi SN, Ouellet D, Turner JT (2018) Model-driven development architectures to solve complex autonomous robotics problems. IEEE Syst J 12(2):1404\u20131413. https:\/\/doi.org\/10.1109\/JSYST.2016.2583403","journal-title":"IEEE Syst J"},{"key":"570_CR18","doi-asserted-by":"publisher","unstructured":"Brugali D, Gherardi L (2016) HyperFlex: a model driven toolchain for designing and configuring software control systems for autonomous robots. Stud Comput Intell 625 https:\/\/doi.org\/10.1007\/978-3-319-26054-9_20","DOI":"10.1007\/978-3-319-26054-9_20"},{"key":"570_CR19","unstructured":"El\u00a0Baccouri H, Guillou G, Babau J-P (2018) Robotic system testing with AMSA framework. In: MoDELS (Workshops), pp 316\u2013325"},{"key":"570_CR20","doi-asserted-by":"publisher","unstructured":"Ramaswamy A, Monsuez B, Tapus A (2014) Saferobots: A model-driven approach for designing robotic software architectures. In: International conference on collaboration technologies and systems .https:\/\/doi.org\/10.1109\/CTS.2014.6867554. IEEE","DOI":"10.1109\/CTS.2014.6867554"},{"key":"570_CR21","doi-asserted-by":"crossref","unstructured":"Baumgartl J, Buchmann T, Henrich D, Westfechtel B (2013) Towards easy robot programming-using DSLS, code generators and software product Lines. In: Proceedings of the 8th International joint conference on software technologies - volume 1: ICSOFT-PT, (ICSOFT 2013), pp 548\u2013554","DOI":"10.5220\/0004585305480554"},{"key":"570_CR22","doi-asserted-by":"publisher","unstructured":"Heinzemann C, Lange R (2018) vTSL\u2014a formally verifiable DSL for specifying robot tasks. In: IEEE\/RSJ International conference on intelligent robots and systems (IROS), pp 8308\u20138314. https:\/\/doi.org\/10.1109\/IROS.2018.8593559","DOI":"10.1109\/IROS.2018.8593559"},{"key":"570_CR23","doi-asserted-by":"publisher","unstructured":"Bencomo N, G\"otz S, Song H, (2019) Models@run.time: a guided tour of the state of the art and research challenges. Int J Softw Syst Model https:\/\/doi.org\/10.1007\/s10270-018-00712-x","DOI":"10.1007\/s10270-018-00712-x"},{"key":"570_CR24","doi-asserted-by":"crossref","unstructured":"Ebert S, Mey J, Sch\u00f6ne R, G\u00f6tz S, A\u00dfmann U (2023) DiNeROS: A model-driven framework for verifiable ros applications with Petri Nets. In: 2023 ACM\/IEEE International conference on model driven engineering languages and systems companion (MODELS-C), pp 791\u2013800. IEEE","DOI":"10.1109\/MODELS-C59198.2023.00127"},{"key":"570_CR25","doi-asserted-by":"publisher","unstructured":"Reisig W (2012) Petri Nets: an introduction vol. 4. Springer, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-642-69968-9","DOI":"10.1007\/978-3-642-69968-9"},{"key":"570_CR26","doi-asserted-by":"publisher","unstructured":"Peterson JL (1977) Petri Nets. ACM Comput Surveys (CSUR) 9(3):223\u2013252. https:\/\/doi.org\/10.1145\/356698.356702","DOI":"10.1145\/356698.356702"},{"key":"570_CR27","first-page":"9","volume":"76","author":"LM Hillah","year":"2009","unstructured":"Hillah LM, Kindler E, Kordon F, Petrucci L, Tr\u00e8ves N (2009) A primer on the Petri Net Markup Language and ISO\/IEC 15909\u20132. Petri Net Newsletter 76:9\u201328","journal-title":"Petri Net Newsletter"},{"key":"570_CR28","doi-asserted-by":"publisher","unstructured":"Jensen K (1983) High-level Petri nets. In: applications and theory of Petri Nets: selected papers from the 3rd European workshop on applications and theory of Petri Nets Varenna, Italy, September 27\u201330, 1982 (under Auspices of AFCET, AICA, GI, and EATCS), pp 166\u2013180. https:\/\/doi.org\/10.1007\/978-3-642-69028-0_12 . Springer","DOI":"10.1007\/978-3-642-69028-0_12"},{"key":"570_CR29","doi-asserted-by":"publisher","unstructured":"Berthomieu B, Vernadat F (2006) Time petri nets analysis with TINA. In: Proceedings of the 3rd international conference on the quantitative evaluation of systems, vol 6, pp 123\u2013124.https:\/\/doi.org\/10.1109\/QEST.2006.56","DOI":"10.1109\/QEST.2006.56"},{"key":"570_CR30","unstructured":"Rosjava. Accessed: 2023-01-30 (2017). http:\/\/wiki.ros.org\/rosjava"},{"key":"570_CR31","doi-asserted-by":"publisher","unstructured":"Behrmann G, David A, Larsen KG (2004) A tutorial on Uppaal. Formal methods for the design of real-time systems, 200\u2013236 https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"570_CR32","unstructured":"Holzmann GJ (2004) The SPIN model checker: primer and reference manual vol 1003. Addison-Wesley, Reading"},{"issue":"5","key":"570_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3342355","volume":"52","author":"M Luckcuck","year":"2019","unstructured":"Luckcuck M, Farrell M, Dennis LA, Dixon C, Fisher M (2019) Formal specification and verification of autonomous robotic systems: a survey. ACM Comput Surveys 52(5):1\u201341. https:\/\/doi.org\/10.1145\/3342355","journal-title":"ACM Comput Surveys"},{"key":"570_CR34","doi-asserted-by":"publisher","first-page":"1021","DOI":"10.1016\/j.cola.2020.101021","volume":"62","author":"Silva E de Ara\u00fajo","year":"2021","unstructured":"de Ara\u00fajo Silva E, Valentin E, Carvalho JRH, da Silva Barreto R (2021) A survey of model driven engineering in robotics. J Comput Lang 62:1021. https:\/\/doi.org\/10.1016\/j.cola.2020.101021","journal-title":"J Comput Lang"},{"issue":"4","key":"570_CR35","doi-asserted-by":"publisher","first-page":"2024","DOI":"10.1109\/TII.2014.2341933","volume":"10","author":"F Moutinho","year":"2014","unstructured":"Moutinho F, Gomes L (2014) Asynchronous-channels within Petri net-based GALS distributed embedded systems modeling. Trans Ind Inf 10(4):2024\u20132033. https:\/\/doi.org\/10.1109\/TII.2014.2341933","journal-title":"Trans Ind Inf"},{"key":"570_CR36","unstructured":"Bera D et al.: (2014) Petri nets for modeling robots. PhD thesis, Einhofen University of Technology"},{"key":"570_CR37","doi-asserted-by":"publisher","unstructured":"Milutinovic D, Lima P (2002) Petri net models of robotic tasks. In: Proceedings 2002 IEEE international conference on robotics and automation, vol 4, pp 4059\u20134064. https:\/\/doi.org\/10.1109\/ROBOT.2002.1014376","DOI":"10.1109\/ROBOT.2002.1014376"},{"key":"570_CR38","doi-asserted-by":"publisher","unstructured":"Kotb YT, Beauchemin SS, Barron JL (2007) Petri net-based cooperation in multi-agent systems. In: Fourth Canadian conference on computer and robot vision (CRV), pp 123\u2013130. https:\/\/doi.org\/10.1109\/CRV.2007.49. IEEE","DOI":"10.1109\/CRV.2007.49"},{"issue":"1","key":"570_CR39","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/S0167-6423(02)00109-0","volume":"47","author":"G Hedin","year":"2003","unstructured":"Hedin G, Magnusson E (2003) JastAdd\u2014an aspect-oriented compiler construction system. Sci. Comput. Progr. 47(1):37\u201358","journal-title":"Sci. Comput. Progr."},{"key":"570_CR40","doi-asserted-by":"crossref","unstructured":"Hillah L-M, Kordon F, Petrucci L, Treves N (2010) PNML framework: an extendable reference implementation of the Petri Net Markup Language. In: 31st International conference on applications and theory of petri nets, Braga, Portugal. Springer","DOI":"10.1007\/978-3-642-13675-7_20"},{"key":"570_CR41","doi-asserted-by":"publisher","unstructured":"Almeida PS (1997) Balloon types: controlling sharing of state in data types. In: ECOOP\u201997\u201311th European conference object-oriented programming Jyv\u00e4skyl\u00e4, Finland, pp 32\u201359. https:\/\/doi.org\/10.1007\/BFb0053373 . Springer","DOI":"10.1007\/BFb0053373"},{"key":"570_CR42","doi-asserted-by":"publisher","unstructured":"Jensen K (1996) Coloured petri nets: basic concepts, analysis methods and practical use. Springer, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-662-03241-1","DOI":"10.1007\/978-3-662-03241-1"},{"key":"570_CR43","doi-asserted-by":"publisher","unstructured":"Sch\u00f6ne R, Mey J, Ebert S, G\u00f6tz S, A\u00dfmann U (2022) Incremental causal connection for self-adaptive systems based on relational reference attribute grammars. In: Proceedings of the 25th international conference on model driven engineering languages and systems, pp 1\u201312. https:\/\/doi.org\/10.1145\/3550355.3552460","DOI":"10.1145\/3550355.3552460"},{"key":"570_CR44","doi-asserted-by":"publisher","unstructured":"Minas M, Frey G (2002) Visual PLC-programming using signal interpreted Petri nets. In: Proceedings of the American control conference, vol 6, pp 5019\u20135024. https:\/\/doi.org\/10.1109\/ACC.2002.1025461. IEEE","DOI":"10.1109\/ACC.2002.1025461"},{"key":"570_CR45","unstructured":"Vyatkin V, Hanisch H (2000) Practice of modeling and verification of distributed controllers using signal net systems. In: International workshop on concurrency, specification and programming"},{"key":"570_CR46","doi-asserted-by":"crossref","unstructured":"Berthomieu B, Le Botlan D, Dal Zilio S (2020) Counting Petri net markings from reduction equations. Int J Softw Tools Technol Transfer 22:163\u2013181","DOI":"10.1007\/s10009-019-00519-1"}],"updated-by":[{"DOI":"10.1007\/s11334-024-00582-1","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2024,11,5]],"date-time":"2024-11-05T00:00:00Z","timestamp":1730764800000}}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-024-00570-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-024-00570-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-024-00570-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,5]],"date-time":"2024-12-05T10:38:43Z","timestamp":1733395123000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-024-00570-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,25]]},"references-count":46,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["570"],"URL":"https:\/\/doi.org\/10.1007\/s11334-024-00570-5","relation":{"correction":[{"id-type":"doi","id":"10.1007\/s11334-024-00582-1","asserted-by":"object"}]},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,25]]},"assertion":[{"value":"17 January 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 May 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 June 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 November 2024","order":4,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Correction","order":5,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"A Correction to this paper has been published:","order":6,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"https:\/\/doi.org\/10.1007\/s11334-024-00582-1","URL":"https:\/\/doi.org\/10.1007\/s11334-024-00582-1","order":7,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}