{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T16:13:03Z","timestamp":1783699983318,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,4,12]],"date-time":"2026-04-12T00:00:00Z","timestamp":1775952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"Engineering and Physical Sciences Research Council (EPSRC).","award":["EP\/X02489X\/1"],"award-info":[{"award-number":["EP\/X02489X\/1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,4,12]]},"DOI":"10.1145\/3793656.3793686","type":"proceedings-article","created":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T15:00:53Z","timestamp":1783695653000},"page":"35-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Model-Driven Assurance for Robotic Controllers: A Subterranean Tunnel Inspection Case Study"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-1364-9820","authenticated-orcid":false,"given":"Yasmin","family":"Rafiq","sequence":"first","affiliation":[{"name":"Department of Computer Science, The University of Manchester, Manchester, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9999-7944","authenticated-orcid":false,"given":"Christopher","family":"Bishop","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Manchester, Manchester, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9783-0147","authenticated-orcid":false,"given":"Simon","family":"Watson","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Manchester, Manchester, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1426-1896","authenticated-orcid":false,"given":"Louise A.","family":"Dennis","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Manchester, Manchester, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-7760-4724","authenticated-orcid":false,"given":"Frederic","family":"Wheeler","sequence":"additional","affiliation":[{"name":"Amentum, Warrington, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-2258-7882","authenticated-orcid":false,"given":"John","family":"Brotherhood","sequence":"additional","affiliation":[{"name":"Amentum, University of Manchester, Warrington, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-7563-9394","authenticated-orcid":false,"given":"Marti Morta","family":"Garriga","sequence":"additional","affiliation":[{"name":"Amentum, Warrington, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4771-1446","authenticated-orcid":false,"given":"Robert M.","family":"Hierons","sequence":"additional","affiliation":[{"name":"School of Computer Science, University of Sheffield, Sheffield, South Yorkshire, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,7,10]]},"reference":[{"key":"e_1_3_3_2_2_2","unstructured":"Robert Alexander Tim\u00a0P Kelly Zeshan Kurd and John\u00a0A Mcdermid. 2007. Safety cases for advanced control software: Safety case patterns. (2007)."},{"key":"e_1_3_3_2_3_2","doi-asserted-by":"crossref","unstructured":"Jonathan Bowen and Victoria Stavridou. 1993. Safety-critical systems formal methods and standards. Software engineering journal 8 4 (1993) 189\u2013209.","DOI":"10.1049\/sej.1993.0025"},{"key":"e_1_3_3_2_4_2","first-page":"223","volume-title":"Software Engineering for Self-Adaptive Systems III. Assurances: International Seminar, Dagstuhl Castle, Germany, December 15-19, 2013, Revised Selected and Invited Papers","author":"Calinescu Radu","year":"2018","unstructured":"Radu Calinescu, Simos Gerasimou, Kenneth Johnson, and Colin Paterson. 2018. Using runtime quantitative verification to provide assurance evidence for self-adaptive software: advances, applications and research challenges. In Software Engineering for Self-Adaptive Systems III. Assurances: International Seminar, Dagstuhl Castle, Germany, December 15-19, 2013, Revised Selected and Invited Papers. Springer, 223\u2013248."},{"key":"e_1_3_3_2_5_2","first-page":"106","volume-title":"International Colloquium on Theoretical Aspects of Computing","author":"Cavalcanti Ana","year":"2021","unstructured":"Ana Cavalcanti, Ziggy Attala, James Baxter, Alvaro Miyazawa, and Pedro Ribeiro. 2021. Model-based engineering for robotics with RoboChart and RoboTool. In International Colloquium on Theoretical Aspects of Computing. Springer, 106\u2013151."},{"key":"e_1_3_3_2_6_2","first-page":"249","volume-title":"Software engineering for robotics","author":"Cavalcanti Ana","year":"2020","unstructured":"Ana Cavalcanti, Will Barnett, James Baxter, Gustavo Carvalho, Madiel\u00a0Conserva Filho, Alvaro Miyazawa, Pedro Ribeiro, and Augusto Sampaio. 2020. RoboStar Technology: A roboticist\u2019s toolbox for combined proof, simulation, and testing. In Software engineering for robotics. Springer, 249\u2013293."},{"key":"e_1_3_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33675-1_2"},{"key":"e_1_3_3_2_8_2","doi-asserted-by":"crossref","unstructured":"Louise\u00a0A Dennis Michael Fisher Nicholas\u00a0K Lincoln Alexei Lisitsa and Sandor\u00a0M Veres. 2016. Practical verification of decision-making in agent-based autonomous systems. Automated Software Engineering 23 3 (2016) 305\u2013359.","DOI":"10.1007\/s10515-014-0168-9"},{"key":"e_1_3_3_2_9_2","doi-asserted-by":"crossref","unstructured":"Michael Fisher Louise Dennis and Matt Webster. 2013. Verifying autonomous systems. Commun. ACM 56 9 (2013) 84\u201393.","DOI":"10.1145\/2494558"},{"key":"e_1_3_3_2_10_2","doi-asserted-by":"crossref","unstructured":"Michael Fisher Viviana Mascardi Kristin\u00a0Yvonne Rozier Bernd-Holger Schlingloff Michael Winikoff and Neil Yorke-Smith. 2021. Towards a framework for certification of reliable autonomous systems. Autonomous Agents and Multi-Agent Systems 35 1 (2021) 8.","DOI":"10.1007\/s10458-020-09487-2"},{"key":"e_1_3_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"e_1_3_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS51672.2020.00017"},{"key":"e_1_3_3_2_13_2","doi-asserted-by":"crossref","unstructured":"J\u00e9r\u00e9mie Guiochet. 2016. Hazard analysis of human\u2013robot interactions with HAZOP\u2013UML. Safety science 84 (2016) 225\u2013237.","DOI":"10.1016\/j.ssci.2015.12.017"},{"key":"e_1_3_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2015.25"},{"key":"e_1_3_3_2_15_2","unstructured":"Richard Hawkins Matt Osborne Mike Parsons Mark Nicholson John McDermid and Ibrahim Habli. 2022. Guidance on the safety assurance of autonomous systems in complex environments (sace). arXiv preprint arXiv:https:\/\/arXiv.org\/abs\/2208.00853 (2022)."},{"key":"e_1_3_3_2_16_2","unstructured":"Richard Hawkins Colin Paterson Chiara Picardi Yan Jia Radu Calinescu and Ibrahim Habli. 2021. Guidance on the assurance of machine learning in autonomous systems (AMLAS). arXiv preprint arXiv:https:\/\/arXiv.org\/abs\/2102.01564 (2021)."},{"key":"e_1_3_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1109\/DASC.2005.1563469"},{"key":"e_1_3_3_2_18_2","doi-asserted-by":"crossref","unstructured":"Maryam Kamali Louise\u00a0A Dennis Owen McAree Michael Fisher and Sandor\u00a0M Veres. 2017. Formal verification of autonomous vehicle platooning. Science of computer programming 148 (2017) 88\u2013106.","DOI":"10.1016\/j.scico.2017.05.006"},{"key":"e_1_3_3_2_19_2","doi-asserted-by":"publisher","unstructured":"Michael Luckcuck Marie Farrell Louise\u00a0A. Dennis Clare Dixon and Michael Fisher. 2019. Formal Specification and Verification of Autonomous Robotic Systems: A Survey. Comput. Surveys 52 5 (2019) 1\u201341. 10.1145\/3342355","DOI":"10.1145\/3342355"},{"key":"e_1_3_3_2_20_2","doi-asserted-by":"crossref","unstructured":"Alvaro Miyazawa Pedro Ribeiro Wei Li Ana Cavalcanti Jon Timmis and Jim Woodcock. 2019. RoboChart: modelling and verification of the functional behaviour of robotic applications. Software & Systems Modeling 18 5 (2019) 3097\u20133149.","DOI":"10.1007\/s10270-018-00710-z"},{"key":"e_1_3_3_2_21_2","volume-title":"Formal methods and the certification of critical systems","author":"Rushby John","year":"1993","unstructured":"John Rushby. 1993. Formal methods and the certification of critical systems. Vol.\u00a037. SRI International, Computer Science Laboratory."},{"key":"e_1_3_3_2_22_2","doi-asserted-by":"crossref","unstructured":"Minghui Sun Smitha Gautham Quanbo Ge Carl Elks and Cody Fleming. 2024. Defining and characterizing model-based safety assessment: A review. Safety science 172 (2024) 106425.","DOI":"10.1016\/j.ssci.2024.106425"},{"key":"e_1_3_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_23"},{"key":"e_1_3_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2013.6696493"},{"key":"e_1_3_3_2_25_2","doi-asserted-by":"crossref","unstructured":"Kangfeng Ye Ana Cavalcanti Simon Foster Alvaro Miyazawa and Jim Woodcock. 2022. Probabilistic modelling and verification using RoboChart and PRISM. Software and Systems Modeling 21 2 (2022) 667\u2013716.","DOI":"10.1007\/s10270-021-00916-8"}],"event":{"name":"FormaliSE '26: IEEE\/ACM 14th International Conference on Formal Methods in Software Engineering","location":"Rio de Janeiro Brazil","acronym":"FormaliSE '26","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the IEEE\/ACM 14th International Conference on Formal Methods in Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3793656.3793686","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T15:21:51Z","timestamp":1783696911000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3793656.3793686"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,4,12]]},"references-count":24,"alternative-id":["10.1145\/3793656.3793686","10.1145\/3793656"],"URL":"https:\/\/doi.org\/10.1145\/3793656.3793686","relation":{},"subject":[],"published":{"date-parts":[[2026,4,12]]},"assertion":[{"value":"2026-07-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}