{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,20]],"date-time":"2025-08-20T12:59:50Z","timestamp":1755694790607,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,6,2]],"date-time":"2018-06-02T00:00:00Z","timestamp":1527897600000},"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,6,2]]},"DOI":"10.1145\/3193992.3193996","type":"proceedings-article","created":{"date-parts":[[2018,7,19]],"date-time":"2018-07-19T13:05:12Z","timestamp":1532005512000},"page":"2-9","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Formal verification of complex robotic systems on resource-constrained platforms"],"prefix":"10.1145","author":[{"given":"Mohammed","family":"Foughali","sequence":"first","affiliation":[{"name":"Universit\u00e9 de Toulouse, CNRS, Toulouse, France"}]},{"given":"Bernard","family":"Berthomieu","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Toulouse, CNRS, Toulouse, France"}]},{"given":"Silvano Dal","family":"Zilio","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Toulouse, CNRS, Toulouse, France"}]},{"given":"Pierre-Emmanuel","family":"Hladik","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Toulouse, CNRS, Toulouse, France"}]},{"given":"F\u00e9lix","family":"Ingrand","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Toulouse, CNRS, Toulouse, France"}]},{"given":"Anthony","family":"Mallet","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Toulouse, CNRS, Toulouse, France"}]}],"member":"320","published-online":{"date-parts":[[2018,6,2]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2012.09.005"},{"key":"e_1_3_2_1_2_1","volume-title":"Silvano Dal Zilio, and Didier Le Botlan","author":"Abid Nouha","year":"2012","unstructured":"Nouha Abid , Silvano Dal Zilio, and Didier Le Botlan . 2012 . Real-Time Specification Patterns and Tools. In Formal Methods for Industrial Critical Systems . 1--15. Nouha Abid, Silvano Dal Zilio, and Didier Le Botlan. 2012. Real-Time Specification Patterns and Tools. In Formal Methods for Industrial Critical Systems. 1--15."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1177\/027836499801700402"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"B. Berthomieu J.-P. Bodeveix P. Farail M. Filali H. Garavel P. Gaufillet F. Lang and F. Vernadat. 2008. Fiacre: an Intermediate Language for Model Verification in the Topcased Environment. In ERTSS.  B. Berthomieu J.-P. Bodeveix P. Farail M. Filali H. Garavel P. Gaufillet F. Lang and F. Vernadat. 2008. Fiacre: an Intermediate Language for Model Verification in the Topcased Environment. In ERTSS.","DOI":"10.1007\/978-3-642-01924-1_15"},{"key":"e_1_3_2_1_6_1","volume-title":"IFIP Congress.","author":"Berthomieu Bernard","year":"1983","unstructured":"Bernard Berthomieu and Miguel Menasche . 1983 . An enumerative approach for analyzing time Petri nets . In IFIP Congress. Bernard Berthomieu and Miguel Menasche. 1983. An enumerative approach for analyzing time Petri nets. In IFIP Congress."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207540412331312688"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSREW.2014.40"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.97299"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Giuseppe Cicala Ali Khalili Giorgio Metta Lorenzo Natale Shashank Pathak Luca Pulina and Armando Tacchella. 2016. Engineering approaches and methods to verify software in autonomous systems. In IAS.  Giuseppe Cicala Ali Khalili Giorgio Metta Lorenzo Natale Shashank Pathak Luca Pulina and Armando Tacchella. 2016. Engineering approaches and methods to verify software in autonomous systems. In IAS.","DOI":"10.1007\/978-3-319-08338-4_121"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2004.05.003"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-1021-7_26"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Mohammed Foughali. 2017. Toward a Correct-and-Scalable Verification of Concurrent Robotic Systems: Insights on Formalisms and Tools. In ACSD.  Mohammed Foughali. 2017. Toward a Correct-and-Scalable Verification of Concurrent Robotic Systems: Insights on Formalisms and Tools. In ACSD.","DOI":"10.1109\/ACSD.2017.10"},{"volume-title":"Model Checking Real-Time Properties on the Functional Layer of Autonomous Robots. In International Conference on Formal Engineering Methods. Springer, 383--399","author":"Foughali M.","key":"e_1_3_2_1_14_1","unstructured":"M. Foughali , B. Berthomieu , S. Dal Zilio , F. Ingrand , and A. Mallet . 2016 . Model Checking Real-Time Properties on the Functional Layer of Autonomous Robots. In International Conference on Formal Engineering Methods. Springer, 383--399 . M. Foughali, B. Berthomieu, S. Dal Zilio, F. Ingrand, and A. Mallet. 2016. Model Checking Real-Time Properties on the Functional Layer of Autonomous Robots. In International Conference on Formal Engineering Methods. Springer, 383--399."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Nicolas Gobillot Fabrice Guet David Doose Christophe Grand Charles Lesire and Luca Santinelli. 2016. Measurement-based real-time analysis of robotic software architectures. In IROS.  Nicolas Gobillot Fabrice Guet David Doose Christophe Grand Charles Lesire and Luca Santinelli. 2016. Measurement-based real-time analysis of robotic software architectures. In IROS.","DOI":"10.1109\/IROS.2016.7759509"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/3101290.3101303"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11164-3_20"},{"key":"e_1_3_2_1_18_1","volume-title":"13th IEEE International Symposium on. IEEE, 201--208","author":"Kargahi Mehdi","year":"2005","unstructured":"Mehdi Kargahi and Ali Movaghar . 2005 . Non-preemptive earliest-deadline-first scheduling policy: a performance study. In Modeling, Analysis, and Simulation of Computer and Telecommunication Systems, 2005 . 13th IEEE International Symposium on. IEEE, 201--208 . Mehdi Kargahi and Ali Movaghar. 2005. Non-preemptive earliest-deadline-first scheduling policy: a performance study. In Modeling, Analysis, and Simulation of Computer and Telecommunication Systems, 2005. 13th IEEE International Symposium on. IEEE, 201--208."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11562948_32"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDT.2006.28"},{"volume-title":"Robotics and Automation (ICRA), 2010 IEEE International Conference on. IEEE, 4627--4632","author":"Mallet A.","key":"e_1_3_2_1_22_1","unstructured":"A. Mallet , C. Pasteur , M. Herrb , S. Lemaignan , and F. Ingrand . 2010. GenoM3: Building middleware-independent robotic components . In Robotics and Automation (ICRA), 2010 IEEE International Conference on. IEEE, 4627--4632 . A. Mallet, C. Pasteur, M. Herrb, S. Lemaignan, and F. Ingrand. 2010. GenoM3: Building middleware-independent robotic components. In Robotics and Automation (ICRA), 2010 IEEE International Conference on. IEEE, 4627--4632."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"P. M. Merlin and D. J. Farber. 1976. Recoverability of Communication Protocols: Implications of a Theoretical Study. IEEE transactions on Communications 24 9 (1976) 1036--1043.  P. M. Merlin and D. J. Farber. 1976. Recoverability of Communication Protocols: Implications of a Theoretical Study. IEEE transactions on Communications 24 9 (1976) 1036--1043.","DOI":"10.1109\/TCOM.1976.1093424"},{"volume-title":"Automatic Property Checking of Robotic Applications. In The International Conference on Intelligent Robots and Systems.","author":"Miyazawa A.","key":"e_1_3_2_1_24_1","unstructured":"A. Miyazawa , P. Ribeiro , W. Li , A. L. C. Cavalcanti , and J. Timmis . 2017 . Automatic Property Checking of Robotic Applications. In The International Conference on Intelligent Robots and Systems. A. Miyazawa, P. Ribeiro, W. Li, A. L. C. Cavalcanti, and J. Timmis. 2017. Automatic Property Checking of Robotic Applications. In The International Conference on Intelligent Robots and Systems."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECRTS.2005.2"},{"key":"e_1_3_2_1_26_1","volume-title":"ICRA workshop on open source software","volume":"3","author":"Quigley Morgan","year":"2009","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 ICRA workshop on open source software , Vol. 3 . Kobe, 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 ICRA workshop on open source software, Vol. 3. Kobe, 5."},{"key":"e_1_3_2_1_27_1","volume-title":"ICRA workshop on open source software","volume":"3","author":"Quigley M.","unstructured":"M. Quigley , B. Gerkey , K. Conley , J. Faust , T. Foote , J. Leibs , E. Berger , R. Wheeler , and A. Y. Ng . 2009. ROS: an open-source Robot Operating System . In ICRA workshop on open source software , Vol. 3 . Kobe, 5. M. Quigley, B. Gerkey, K. Conley, J. Faust, T. Foote, J. Leibs, E. Berger, R. Wheeler, and A. Y. Ng. 2009. ROS: an open-source Robot Operating System. In ICRA workshop on open source software, Vol. 3. Kobe, 5."},{"volume-title":"Understanding concurrent systems","author":"Roscoe Andrew William","key":"e_1_3_2_1_28_1","unstructured":"Andrew William Roscoe . 2010. Understanding concurrent systems . Springer Science & Business Media . Andrew William Roscoe. 2010. Understanding concurrent systems. Springer Science & Business Media."},{"key":"e_1_3_2_1_29_1","first-page":"629","article-title":"Analysis of first-come-first-serve parallel job scheduling","volume":"98","author":"Schwiegelshohn Uwe","year":"1998","unstructured":"Uwe Schwiegelshohn and Ramin Yahyapour . 1998 . Analysis of first-come-first-serve parallel job scheduling . In SODA , Vol. 98. 629 -- 638 . Uwe Schwiegelshohn and Ramin Yahyapour. 1998. Analysis of first-come-first-serve parallel job scheduling. In SODA, Vol. 98. 629--638.","journal-title":"SODA"},{"key":"e_1_3_2_1_30_1","unstructured":"Jiazheng Shi Steve Goddard Anagh Lal and Shane Farritor. 2004. A real-time model for the robotic highway safety marker system. In RTAS.  Jiazheng Shi Steve Goddard Anagh Lal and Shane Farritor. 2004. A real-time model for the robotic highway safety marker system. In RTAS."},{"key":"e_1_3_2_1_31_1","unstructured":"Reid Simmons Charles Pecheur and G Srinivasan. 2000. Towards Automatic Verification of Autonomous Systems. In IROS.  Reid Simmons Charles Pecheur and G Srinivasan. 2000. Towards Automatic Verification of Autonomous Systems. In IROS."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80435-9"},{"key":"e_1_3_2_1_33_1","unstructured":"John D Sweeney Huan Li Roderic A Grupen and Krithi Ramamritham. 2003. Scalability and schedulability in large coordinated distributed robot systems. In ICRA.  John D Sweeney Huan Li Roderic A Grupen and Krithi Ramamritham. 2003. Scalability and schedulability in large coordinated distributed robot systems. In ICRA."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Kai Weng Wong and Hadas Kress-Gazit. 2016. Need-based coordination for decentralized high-level robot control. In IROS.  Kai Weng Wong and Hadas Kress-Gazit. 2016. Need-based coordination for decentralized high-level robot control. In IROS.","DOI":"10.1109\/IROS.2016.7759346"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2013.6630618"}],"event":{"name":"ICSE '18: 40th International Conference on Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE-CS Computer Society"],"location":"Gothenburg Sweden","acronym":"ICSE '18"},"container-title":["Proceedings of the 6th Conference on Formal Methods in Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3193992.3193996","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3193992.3193996","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T17:49:15Z","timestamp":1750268955000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3193992.3193996"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,2]]},"references-count":35,"alternative-id":["10.1145\/3193992.3193996","10.1145\/3193992"],"URL":"https:\/\/doi.org\/10.1145\/3193992.3193996","relation":{},"subject":[],"published":{"date-parts":[[2018,6,2]]},"assertion":[{"value":"2018-06-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}