{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:25:03Z","timestamp":1750220703574,"version":"3.41.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","license":[{"start":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T00:00:00Z","timestamp":1570492800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Ministero dell\u00f0Istruzione, dell\u00f0Universit\u00e0 e della Ricerca","award":["Dipartimenti di Eccellenza"],"award-info":[{"award-number":["Dipartimenti di Eccellenza"]}]},{"DOI":"10.13039\/501100001459","name":"Ministry of Education - Singapore","doi-asserted-by":"publisher","award":["MOE2018-T2-1-098"],"award-info":[{"award-number":["MOE2018-T2-1-098"]}],"id":[{"id":"10.13039\/501100001459","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2019,10,31]]},"abstract":"<jats:p>\n            This paper presents a methodology that relies on Assume-Guarantee Contracts to decompose the problem of synthesizing control software for a multi-robot system. Initially, each contract describes either a component (\n            <jats:italic>e.g.<\/jats:italic>\n            , a robot) or an aspect of the system. Then, the design problem is decomposed into different synthesis and verification sub-problems, allowing to tackle the complexity involved in the design process. The design problem is then recomposed by exploiting the rigorousness provided by contracts. This allows us to achieve system-level simulation capable to be used for validating the entire design. Once validated, the software synthesized during the process can be integrated into Robot Operating System (ROS) nodes and executed using state-of-the-practice packages and tools for modern robotic systems.\n          <\/jats:p>\n          <jats:p>We apply the methodology to generate a control strategy for an autonomous goods transportation system. Our results show a massive reduction of the time required to obtain automatically the control software implementing a multi-robot mission.<\/jats:p>","DOI":"10.1145\/3358197","type":"journal-article","created":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T13:13:05Z","timestamp":1570713185000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Compositional Design of Multi-Robot Systems Control Software on ROS"],"prefix":"10.1145","volume":"18","author":[{"given":"Stefano","family":"Spellini","sequence":"first","affiliation":[{"name":"University of Verona, Verona, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6224-4313","authenticated-orcid":false,"given":"Michele","family":"Lora","sequence":"additional","affiliation":[{"name":"Singapore University of Technology and Design, Singapore, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4404-5791","authenticated-orcid":false,"given":"Franco","family":"Fummi","sequence":"additional","affiliation":[{"name":"University of Verona, Verona, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4843-5391","authenticated-orcid":false,"given":"Sudipta","family":"Chattopadhyay","sequence":"additional","affiliation":[{"name":"Singapore University of Technology and Design, Singapore, Singapore"}]}],"member":"320","published-online":{"date-parts":[[2019,10,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/3283535.3283545"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.7873\/DATE.2015.0913"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Albert Benveniste et al. 2018. Contracts for system design. Foundations and Trends\u00ae in Electronic Design Automation 12 2--3 (2018) 124--400.  Albert Benveniste et al. 2018. Contracts for system design. Foundations and Trends\u00ae in Electronic Design Automation 12 2--3 (2018) 124--400.","DOI":"10.1561\/1000000053"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2011.08.007"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1155\/2010\/436328"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSD.2012.96"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2001.933002"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"volume-title":"2017 ACM\/IEEE 8th International Conference on Cyber-Physical Systems (ICCPS). IEEE, 239--248","author":"Desai Ankush","key":"e_1_2_1_9_1","unstructured":"Ankush Desai , Indranil Saha , Jianqiao Yang , Shaz Qadeer , and Sanjit A. Seshia . 2017. Drona: A framework for safe distributed mobile robotics . In 2017 ACM\/IEEE 8th International Conference on Cyber-Physical Systems (ICCPS). IEEE, 239--248 . Ankush Desai, Indranil Saha, Jianqiao Yang, Shaz Qadeer, and Sanjit A. Seshia. 2017. Drona: A framework for safe distributed mobile robotics. In 2017 ACM\/IEEE 8th International Conference on Cyber-Physical Systems (ICCPS). IEEE, 239--248."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_18"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.30720"},{"key":"e_1_2_1_12_1","volume-title":"INCOSE International Symposium","volume":"26","author":"Yishai","unstructured":"Yishai A. Feldman and Henry Broodney. 2016. A cognitive journey for requirements engineering . In INCOSE International Symposium , Vol. 26 . Wiley Online Library, 430--444. Yishai A. Feldman and Henry Broodney. 2016. A cognitive journey for requirements engineering. In INCOSE International Symposium, Vol. 26. Wiley Online Library, 430--444."},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of IEEE Conference on Control Applications (CCA)","author":"Filippidis Ioannis","year":"2016","unstructured":"Ioannis Filippidis , Sumanth Dathathri , Scott C. Livingston , Necmiye Ozay , and Richard M. Murray . 2016. Control design for hybrid systems with TuLiP: The temporal logic planning toolbox . In Proceedings of IEEE Conference on Control Applications (CCA) 2016 . 1030--1041. Ioannis Filippidis, Sumanth Dathathri, Scott C. Livingston, Necmiye Ozay, and Richard M. Murray. 2016. Control design for hybrid systems with TuLiP: The temporal logic planning toolbox. In Proceedings of IEEE Conference on Control Applications (CCA) 2016. 1030--1041."},{"volume-title":"2010 IEEE\/RSJ International Conference on Intelligent Robots and Systems. 1988--1993","author":"Finucane C.","key":"e_1_2_1_14_1","unstructured":"C. Finucane and H. Kress-Gazit . 2010. LTLMoP: Experimenting with language, temporal logic and robot control . In 2010 IEEE\/RSJ International Conference on Intelligent Robots and Systems. 1988--1993 . C. Finucane and H. Kress-Gazit. 2010. LTLMoP: Experimenting with language, temporal logic and robot control. In 2010 IEEE\/RSJ International Conference on Intelligent Robots and Systems. 1988--1993."},{"key":"e_1_2_1_15_1","first-page":"286","article-title":"Moving from co-simulation to simulation for effective smart systems design","volume":"2014","author":"Fummi Franco","year":"2014","unstructured":"Franco Fummi , Michele Lora , Francesco Stefanni , Dimitrios Trachanis , Jahn Vanhese , and Sara Vinco . 2014 . Moving from co-simulation to simulation for effective smart systems design . In Proceedings of IEEE\/ACM Design Automation and Test in Europe (DATE) 2014. 286 . Franco Fummi, Michele Lora, Francesco Stefanni, Dimitrios Trachanis, Jahn Vanhese, and Sara Vinco. 2014. Moving from co-simulation to simulation for effective smart systems design. In Proceedings of IEEE\/ACM Design Automation and Test in Europe (DATE) 2014. 286.","journal-title":"Proceedings of IEEE\/ACM Design Automation and Test in Europe (DATE)"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1177\/0278364904045564"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2012.02.004"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.898830"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of IEEE\/RSJ International Conference on Intelligent Robotics and Systems (IROS)","volume":"3","author":"Koenig N.","unstructured":"N. Koenig and A. Howard . 2004. Design and use paradigms for gazebo, an open-source multi-robot simulator . In Proceedings of IEEE\/RSJ International Conference on Intelligent Robotics and Systems (IROS) , Vol. 3 . IEEE, 2149--2154. http:\/\/ieeexplore.ieee.org\/document\/1389727\/. N. Koenig and A. Howard. 2004. Design and use paradigms for gazebo, an open-source multi-robot simulator. In Proceedings of IEEE\/RSJ International Conference on Intelligent Robotics and Systems (IROS), Vol. 3. IEEE, 2149--2154. http:\/\/ieeexplore.ieee.org\/document\/1389727\/."},{"key":"e_1_2_1_21_1","volume-title":"Robot challenges: Toward development of verification and synthesis techniques","author":"Kress-Gazit Hadas","year":"2011","unstructured":"Hadas Kress-Gazit . 2011. Robot challenges: Toward development of verification and synthesis techniques . IEEE Robotics 8 Automation Magazine 18, 3 ( 2011 ), 22--23. Hadas Kress-Gazit. 2011. Robot challenges: Toward development of verification and synthesis techniques. IEEE Robotics 8 Automation Magazine 18, 3 (2011), 22--23."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2009.2030225"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30482-1_23"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2019.2909209"},{"volume-title":"IEEE International Conference on Robotics and Automation (ICRA). 4192--4199","author":"Maniatopoulos S.","key":"e_1_2_1_25_1","unstructured":"S. Maniatopoulos , P. Schillinger , V. Pong , D. C. Conner , and H. Kress-Gazit . 2016. Reactive high-level behavior synthesis for an Atlas humanoid robot . In IEEE International Conference on Robotics and Automation (ICRA). 4192--4199 . S. Maniatopoulos, P. Schillinger, V. Pong, D. C. Conner, and H. Kress-Gazit. 2016. Reactive high-level behavior synthesis for an Atlas humanoid robot. In IEEE International Conference on Robotics and Automation (ICRA). 4192--4199."},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"J. W. McDonald Hayhurst and D. C. Conner. 2018. Towards capability-based synthesis of executable robot behaviors. In SoutheastCon 2018. 1--8.  J. W. McDonald Hayhurst and D. C. Conner. 2018. Towards capability-based synthesis of executable robot behaviors. In SoutheastCon 2018. 1--8.","DOI":"10.1109\/SECON.2018.8479047"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of VMCAI","author":"Nir Piterman Amir Pnueli","year":"2006","unstructured":"Amir Pnueli Nir Piterman and Yaniv Saar . 2006 . Synthesis of reactive(1) designs . In Proceedings of VMCAI 2006. Amir Pnueli Nir Piterman and Yaniv Saar. 2006. Synthesis of reactive(1) designs. In Proceedings of VMCAI 2006."},{"volume-title":"2014 Twelfth ACM\/IEEE Conference on Formal Methods and Models for Codesign (MEMOCODE). 104--113","author":"Nuzzo P.","key":"e_1_2_1_28_1","unstructured":"P. Nuzzo , A. Iannopollo , S. Tripakis , and A. Sangiovanni-Vincentelli . 2014. Are interface theories equivalent to contract theories? . In 2014 Twelfth ACM\/IEEE Conference on Formal Methods and Models for Codesign (MEMOCODE). 104--113 . P. Nuzzo, A. Iannopollo, S. Tripakis, and A. Sangiovanni-Vincentelli. 2014. Are interface theories equivalent to contract theories?. In 2014 Twelfth ACM\/IEEE Conference on Formal Methods and Models for Codesign (MEMOCODE). 104--113."},{"key":"e_1_2_1_29_1","first-page":"839","article-title":"CHASE: Contract-based requirement engineering for cyber-physical system design","volume":"2018","author":"Nuzzo Pierluigi","year":"2018","unstructured":"Pierluigi Nuzzo , Michele Lora , Yishai A Feldman , and Alberto Sangiovanni-Vincentelli . 2018 . CHASE: Contract-based requirement engineering for cyber-physical system design . In Proceedings of IEEE\/ACM Design Automation and Test in Europe (DATE) 2018. 839 -- 844 . Pierluigi Nuzzo, Michele Lora, Yishai A Feldman, and Alberto Sangiovanni-Vincentelli. 2018. CHASE: Contract-based requirement engineering for cyber-physical system design. In Proceedings of IEEE\/ACM Design Automation and Test in Europe (DATE) 2018. 839--844.","journal-title":"Proceedings of IEEE\/ACM Design Automation and Test in Europe (DATE)"},{"key":"e_1_2_1_30_1","volume-title":"Sangiovanni-Vincentelli","author":"Nuzzo Pierluigi","year":"2018","unstructured":"Pierluigi Nuzzo and Alberto L . Sangiovanni-Vincentelli . 2018 . Hierarchical system design with vertical contracts. In Principles of Modeling. Springer , 360--382. Pierluigi Nuzzo and Alberto L. Sangiovanni-Vincentelli. 2018. Hierarchical system design with vertical contracts. In Principles of Modeling. Springer, 360--382."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2015.2453253"},{"key":"e_1_2_1_32_1","volume-title":"INCOSE International Symposium","volume":"25","author":"Nuzzo Pierluigi","unstructured":"Pierluigi Nuzzo , Alberto L. Sangiovanni-Vincentelli , and Richard M. Murray . 2015. Methodology and tools for next generation cyber-physical systems: The iCyPhy approach . In INCOSE International Symposium , Vol. 25 . Wiley Online Library, 235--249. Pierluigi Nuzzo, Alberto L. Sangiovanni-Vincentelli, and Richard M. Murray. 2015. Methodology and tools for next generation cyber-physical systems: The iCyPhy approach. In INCOSE International Symposium, Vol. 25. Wiley Online Library, 235--249."},{"key":"e_1_2_1_33_1","unstructured":"Open Source Robotics Foundation (OSRF). 2018. Gazebo Simulator. https:\/\/www.openrobotics.org\/.  Open Source Robotics Foundation (OSRF). 2018. Gazebo Simulator. https:\/\/www.openrobotics.org\/."},{"key":"e_1_2_1_34_1","volume-title":"Susanne Graf, Albert Benveniste, Daniela Cancila, Arnaud Cuccuru, Sebastien Gerard, Francois Terrier, Werner Damm, Alberto Ferrari, et al.","author":"Passerone Roberto","year":"2009","unstructured":"Roberto Passerone , Imene Ben Hafaiedh , Susanne Graf, Albert Benveniste, Daniela Cancila, Arnaud Cuccuru, Sebastien Gerard, Francois Terrier, Werner Damm, Alberto Ferrari, et al. 2009 . Metamodels in Europe : Languages, tools, and applications. IEEE Design 8 Test of Computers 26, 3 (2009), 38--53. Roberto Passerone, Imene Ben Hafaiedh, Susanne Graf, Albert Benveniste, Daniela Cancila, Arnaud Cuccuru, Sebastien Gerard, Francois Terrier, Werner Damm, Alberto Ferrari, et al. 2009. Metamodels in Europe: Languages, tools, and applications. IEEE Design 8 Test of Computers 26, 3 (2009), 38--53."},{"key":"e_1_2_1_35_1","volume-title":"IEEE International Conference on Robotics and Automation (ICRA)","volume":"3","author":"Quigley Morgan","unstructured":"Morgan Quigley , Ken Conley , Brian Gerkey , Josh Faust , Tully Foote , Jeremy Leibs , Rob Wheeler , and Andrew Y. Ng . 2009. ROS: An open-source robot operating system . In IEEE International Conference on Robotics and Automation (ICRA) , Vol. 3 . Kobe, Japan, 5. Morgan Quigley, Ken Conley, Brian Gerkey, Josh Faust, Tully Foote, Jeremy Leibs, Rob Wheeler, and Andrew Y. Ng. 2009. ROS: An open-source robot operating system. In IEEE International Conference on Robotics and Automation (ICRA), Vol. 3. Kobe, Japan, 5."},{"key":"e_1_2_1_36_1","unstructured":"Robotis. 2017. Turtlebot3. http:\/\/www.robotis.us\/turtlebot-3\/.  Robotis. 2017. Turtlebot3. http:\/\/www.robotis.us\/turtlebot-3\/."},{"volume-title":"2018 International Conference on Hardware\/Software Codesign and System Synthesis (CODES+ISSS). 1--2.","author":"Spellini S.","key":"e_1_2_1_38_1","unstructured":"S. Spellini , M. Lora , S. Chattopadhyay , and F. Fummi . 2018. Work-in-progress: Introducing assume-guarantee contracts for verifying robotic applications . In 2018 International Conference on Hardware\/Software Codesign and System Synthesis (CODES+ISSS). 1--2. S. Spellini, M. Lora, S. Chattopadhyay, and F. Fummi. 2018. Work-in-progress: Introducing assume-guarantee contracts for verifying robotic applications. In 2018 International Conference on Hardware\/Software Codesign and System Synthesis (CODES+ISSS). 1--2."},{"volume-title":"2017 First IEEE International Conference on Robotic Computing (IRC). 188--195","author":"Wong K. W.","key":"e_1_2_1_39_1","unstructured":"K. W. Wong and H. Kress-Gazit . 2017. From high-level task specification to robot operating system (ROS) implementation . In 2017 First IEEE International Conference on Robotic Computing (IRC). 188--195 . K. W. Wong and H. Kress-Gazit. 2017. From high-level task specification to robot operating system (ROS) implementation. In 2017 First IEEE International Conference on Robotic Computing (IRC). 188--195."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358197","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3358197","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:32:58Z","timestamp":1750199578000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358197"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,8]]},"references-count":38,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2019,10,31]]}},"alternative-id":["10.1145\/3358197"],"URL":"https:\/\/doi.org\/10.1145\/3358197","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2019,10,8]]},"assertion":[{"value":"2019-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-10-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}