{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T16:16:30Z","timestamp":1778256990700,"version":"3.51.4"},"reference-count":96,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2021,5,10]],"date-time":"2021-05-10T00:00:00Z","timestamp":1620604800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"\u201cRobotics and AI in Hazardous Environments\u201d","award":["EP\/R026084 (RAIN), EP\/R026173 (ORCA), and EP\/R026092 (FAIR-SPACE)"],"award-info":[{"award-number":["EP\/R026084 (RAIN), EP\/R026173 (ORCA), and EP\/R026092 (FAIR-SPACE)"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2021,10,31]]},"abstract":"<jats:p>\n            When applying formal verification to a system that interacts with the real world, we must use a\n            <jats:italic>model<\/jats:italic>\n            of the environment. This model represents an\n            <jats:italic>abstraction<\/jats:italic>\n            of the actual environment, so it is necessarily incomplete and hence presents an issue for system verification. If the actual environment matches the model, then the verification is correct; however, if the environment falls outside the abstraction captured by the model, then we cannot guarantee that the system is well behaved. A solution to this problem consists in exploiting the model of the environment used for statically verifying the system\u2019s behaviour and, if the verification succeeds, using it also for validating the model against the real environment via runtime verification. The article discusses this approach and demonstrates its feasibility by presenting its implementation on top of a framework integrating the Agent Java PathFinder model checker. A high-level Domain Specific Language is used to model the environment in a user-friendly way; the latter is then compiled to trace expressions for both static formal verification and runtime verification. To evaluate our approach, we apply it to two different case studies: an autonomous cruise control system and a simulation of the Mars Curiosity rover.\n          <\/jats:p>","DOI":"10.1145\/3447246","type":"journal-article","created":{"date-parts":[[2021,5,10]],"date-time":"2021-05-10T22:17:21Z","timestamp":1620685041000},"page":"1-43","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Toward a Holistic Approach to Verification and Validation of Autonomous Cognitive Systems"],"prefix":"10.1145","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8711-4670","authenticated-orcid":false,"given":"Angelo","family":"Ferrando","sequence":"first","affiliation":[{"name":"The University of Manchester, Manchester, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Louise A.","family":"Dennis","sequence":"additional","affiliation":[{"name":"The University of Manchester, Manchester, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rafael C.","family":"Cardoso","sequence":"additional","affiliation":[{"name":"The University of Manchester, Manchester, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[{"name":"The University of Manchester, Manchester, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6297-2011","authenticated-orcid":false,"given":"Davide","family":"Ancona","sequence":"additional","affiliation":[{"name":"University of Genova, Genova, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viviana","family":"Mascardi","sequence":"additional","affiliation":[{"name":"University of Genova, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,5,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11558590_14"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing, Luigi Logrippo (Ed.). ACM, 139--152","author":"Alur Rajeev","unstructured":"Rajeev Alur , Tom\u00e1s Feder , and Thomas A. Henzinger . 1991. The benefits of relaxing punctuality . In Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing, Luigi Logrippo (Ed.). ACM, 139--152 . DOI:https:\/\/doi.org\/10.1145\/112600.112613 10.1145\/112600.112613 Rajeev Alur, Tom\u00e1s Feder, and Thomas A. Henzinger. 1991. The benefits of relaxing punctuality. In Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing, Luigi Logrippo (Ed.). ACM, 139--152. DOI:https:\/\/doi.org\/10.1145\/112600.112613"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.871304"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480362.2480620"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems (AAMAS\u201915)","author":"Ancona D.","unstructured":"D. Ancona , D. Briola , A. Ferrando , and V. Mascardi . 2015. Global protocols as first class entities for self-adaptive agents . In Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems (AAMAS\u201915) . 1019--1029. D. Ancona, D. Briola, A. Ferrando, and V. Mascardi. 2015. Global protocols as first class entities for self-adaptive agents. In Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems (AAMAS\u201915). 1019--1029."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of Declarative Agent Languages and Technologies X (DALT\u201912)","author":"Ancona Davide","year":"2012","unstructured":"Davide Ancona , Sophia Drossopoulou , and Viviana Mascardi . 2012 . Automatic generation of self-monitoring MASs from multiparty global session types in Jason . In Proceedings of Declarative Agent Languages and Technologies X (DALT\u201912) . 76--95. Davide Ancona, Sophia Drossopoulou, and Viviana Mascardi. 2012. Automatic generation of self-monitoring MASs from multiparty global session types in Jason. In Proceedings of Declarative Agent Languages and Technologies X (DALT\u201912). 76--95."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3103111.3104037"},{"key":"e_1_2_1_9_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of 16th International Conference on Advances in Practical Applications of Agents, Multi-Agent Systems, and Complexity: The PAAMS Collection","author":"Ancona Davide","unstructured":"Davide Ancona , Angelo Ferrando , Luca Franceschini , and Viviana Mascardi . 2018. Coping with bad agent interaction protocols when monitoring partially observable multiagent systems . In Proceedings of 16th International Conference on Advances in Practical Applications of Agents, Multi-Agent Systems, and Complexity: The PAAMS Collection , Lecture Notes in Computer Science , Vol. 10978 . Springer , 59--71. Davide Ancona, Angelo Ferrando, Luca Franceschini, and Viviana Mascardi. 2018. Coping with bad agent interaction protocols when monitoring partially observable multiagent systems. In Proceedings of 16th International Conference on Advances in Practical Applications of Agents, Multi-Agent Systems, and Complexity: The PAAMS Collection, Lecture Notes in Computer Science, Vol. 10978. Springer, 59--71."},{"key":"e_1_2_1_10_1","volume-title":"Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday.","author":"Ancona Davide","unstructured":"Davide Ancona , Angelo Ferrando , and Viviana Mascardi . 2016. Comparing trace expressions and linear temporal logic for runtime verification . In Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday. Davide Ancona, Angelo Ferrando, and Viviana Mascardi. 2016. Comparing trace expressions and linear temporal logic for runtime verification. In Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday."},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 2017 International Conference on Autonomous Agents and Multiagent Systems (AAMAS\u201917)","author":"Ancona Davide","year":"2017","unstructured":"Davide Ancona , Angelo Ferrando , and Viviana Mascardi . 2017 . Parametric runtime verification of multiagent systems . In Proceedings of the 2017 International Conference on Autonomous Agents and Multiagent Systems (AAMAS\u201917) . ACM, 1457--1459. Davide Ancona, Angelo Ferrando, and Viviana Mascardi. 2017. Parametric runtime verification of multiagent systems. In Proceedings of the 2017 International Conference on Autonomous Agents and Multiagent Systems (AAMAS\u201917). ACM, 1457--1459."},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the 1st Workshop on Architectures, Languages and Paradigms for IoT (ALP4IoT@iFM\u201917)","volume":"264","author":"Ancona Davide","year":"2017","unstructured":"Davide Ancona , Luca Franceschini , Giorgio Delzanno , Maurizio Leotta , Marina Ribaudo , and Filippo Ricca . 2017 . Towards runtime monitoring of Node.js and its application to the Internet of Things . In Proceedings of the 1st Workshop on Architectures, Languages and Paradigms for IoT (ALP4IoT@iFM\u201917) , EPTCS Vol. 264 . 27--42. Davide Ancona, Luca Franceschini, Giorgio Delzanno, Maurizio Leotta, Marina Ribaudo, and Filippo Ricca. 2017. Towards runtime monitoring of Node.js and its application to the Internet of Things. In Proceedings of the 1st Workshop on Architectures, Languages and Paradigms for IoT (ALP4IoT@iFM\u201917), EPTCS Vol. 264. 27--42."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.11.007"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/506147.506151"},{"key":"e_1_2_1_15_1","volume-title":"Principles of Model Checking","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen . 2008. Principles of Model Checking . MIT Press . Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/3283535.3283536"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_60"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201908)","author":"Basin David A.","year":"2008","unstructured":"David A. Basin , Felix Klaedtke , Samuel M\u00fcller , and Birgit Pfitzmann . 2008 . Runtime monitoring of metric first-order temporal properties . In Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201908) , Ramesh Hariharan, Madhavan Mukund, and V. Vinay (Eds.), LIPIcs,Vol. 2. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, 49--60. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS. 2008.1740 10.4230\/LIPIcs.FSTTCS.2008.1740 David A. Basin, Felix Klaedtke, Samuel M\u00fcller, and Birgit Pfitzmann. 2008. Runtime monitoring of metric first-order temporal properties. In Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201908), Ramesh Hariharan, Madhavan Mukund, and V. Vinay (Eds.), LIPIcs,Vol. 2. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, 49--60. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2008.1740"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2000799.2000800"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/8.3.401"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10458-006-5955-7"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"R. H. Bordini J. F. H\u00fcbner and M. Wooldridge. 2007. Programming Multi-agent Systems in AgentSpeak Using Jason. John Wiley & Sons.  R. H. Bordini J. F. H\u00fcbner and M. Wooldridge. 2007. Programming Multi-agent Systems in AgentSpeak Using Jason. John Wiley & Sons.","DOI":"10.1002\/9780470061848"},{"key":"e_1_2_1_24_1","volume-title":"Harvard University Press","author":"Bratman Michael E.","unstructured":"Michael E. Bratman . 1987. Intention, Plans, and Practical Reason . Harvard University Press , Cambridge, MA . Michael E. Bratman. 1987. Intention, Plans, and Practical Reason. Harvard University Press, Cambridge, MA."},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the 29th Italian Conference on Computational Logic. 319--323","author":"Briola Daniela","year":"2014","unstructured":"Daniela Briola , Viviana Mascardi , and Davide Ancona . 2014 . Distributed runtime verification of JADE and jason multiagent systems with prolog . In Proceedings of the 29th Italian Conference on Computational Logic. 319--323 . Daniela Briola, Viviana Mascardi, and Davide Ancona. 2014. Distributed runtime verification of JADE and jason multiagent systems with prolog. In Proceedings of the 29th Italian Conference on Computational Logic. 319--323."},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the ACM International Conference on Interaction Design and Children (IDC\u201914)","author":"Briola D.","unstructured":"D. Briola , V. Mascardi , and D. Ancona . 2014. Distributed runtime verification of JADE multiagent systems . In Proceedings of the ACM International Conference on Interaction Design and Children (IDC\u201914) . D. Briola, V. Mascardi, and D. Ancona. 2014. Distributed runtime verification of JADE multiagent systems. In Proceedings of the ACM International Conference on Interaction Design and Children (IDC\u201914)."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2017.08.013"},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the NASA Formal Methods Symposium (NFM\u201920)","author":"Cardoso R. C.","unstructured":"R. C. Cardoso , M. Farrell , M. Luckcuck , A. Ferrando , and M. Fisher . 2020. Heterogeneous verification of an autonomous curiosity rover . In Proceedings of the NASA Formal Methods Symposium (NFM\u201920) . R. C. Cardoso, M. Farrell, M. Luckcuck, A. Ferrando, and M. Fisher. 2020. Heterogeneous verification of an autonomous curiosity rover. In Proceedings of the NASA Formal Methods Symposium (NFM\u201920)."},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the European Conference on Multi-Agent Systems (EUMAS\u201920)","author":"Cardoso R. C.","unstructured":"R. C. Cardoso , A. Ferrando , L. A. Dennis , and M. Fisher . 2020. An interface for programming verifiable autonomous agents in ROS . In Proceedings of the European Conference on Multi-Agent Systems (EUMAS\u201920) . R. C. Cardoso, A. Ferrando, L. A. Dennis, and M. Fisher. 2020. An interface for programming verifiable autonomous agents in ROS. In Proceedings of the European Conference on Multi-Agent Systems (EUMAS\u201920)."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70848-5_1"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/1661445.1661461"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the 34th Italian Conference on Computational Logic (CEUR Workshop Proceedings), Alberto Casagrande and Eugenio G. Omodeo (Eds.)","volume":"2396","author":"Ciccone Luca","year":"2019","unstructured":"Luca Ciccone , Angelo Ferrando , Davide Ancona , and Viviana Mascardi . 2019 . Timed trace expressions . In Proceedings of the 34th Italian Conference on Computational Logic (CEUR Workshop Proceedings), Alberto Casagrande and Eugenio G. Omodeo (Eds.) , Vol. 2396 . 229--241. Luca Ciccone, Angelo Ferrando, Davide Ancona, and Viviana Mascardi. 2019. Timed trace expressions. In Proceedings of the 34th Italian Conference on Computational Logic (CEUR Workshop Proceedings), Alberto Casagrande and Eugenio G. Omodeo (Eds.), Vol. 2396. 229--241."},{"key":"e_1_2_1_33_1","volume-title":"Peled","author":"Clarke Edmund M.","year":"2000","unstructured":"Edmund M. Clarke , Orna Grumberg , and Doron A . Peled . 2000 . Model Checking. The MIT Press . Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 2000. Model Checking. The MIT Press."},{"key":"e_1_2_1_34_1","volume-title":"Clarke and Bernd-Holger Schlingloff","author":"Edmund","year":"2001","unstructured":"Edmund M. Clarke and Bernd-Holger Schlingloff . 2001 . Model checking. In Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.). Elsevier and MIT Press , 1635--1790. Edmund M. Clarke and Bernd-Holger Schlingloff. 2001. Model checking. In Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.). Elsevier and MIT Press, 1635--1790."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/123768.123784"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.21105\/joss.00617"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40379-3_8"},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the 8th International Workshop on Declarative Agent Languages and Technologies (DALT\u201910)","author":"Dennis L. A.","unstructured":"L. A. Dennis , M. Fisher , N. Lincoln , A. Lisitsa , and S. M. Veres . 2010. Declarative abstractions for agent based hybrid control systems . In Proceedings of the 8th International Workshop on Declarative Agent Languages and Technologies (DALT\u201910) . 96--111. L. A. Dennis, M. Fisher, N. Lincoln, A. Lisitsa, and S. M. Veres. 2010. Declarative abstractions for agent based hybrid control systems. In Proceedings of the 8th International Workshop on Declarative Agent Languages and Technologies (DALT\u201910). 96--111."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-014-0168-9"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-011-0088-x"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-61756-5"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462184"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2011.24"},{"key":"e_1_2_1_45_1","first-page":"141","article-title":"A tutorial on runtime verification","volume":"34","author":"Falcone Yli\u00e8s","year":"2013","unstructured":"Yli\u00e8s Falcone , Klaus Havelund , and Giles Reger . 2013 . A tutorial on runtime verification . Eng. Depend. Softw. Syst. 34 , 01 (2013), 141 -- 175 . Yli\u00e8s Falcone, Klaus Havelund, and Giles Reger. 2013. A tutorial on runtime verification. Eng. Depend. Softw. Syst. 34, 01 (2013), 141--175.","journal-title":"Eng. Depend. Softw. Syst."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03769-7_14"},{"key":"e_1_2_1_47_1","series-title":"Lecture Notes in Computer Science","volume-title":"Pace","author":"Falzon Kevin","year":"2012","unstructured":"Kevin Falzon and Gordon J . Pace . 2012 . Combining testing and runtime verification techniques. In Proceedings of the 8th International Workshop Model-Based Methodologies for Pervasive and Embedded Software (MOMPES\u201912), Ricardo Jorge Machado, Rita Suzana Pitangueira Maciel, Julia Rubin, and Goetz Botterweck (Eds.), Lecture Notes in Computer Science ,Vol. 7706. Springer , 38--57. DOI:https:\/\/doi.org\/10.1007\/978-3-642-38209-3_3 10.1007\/978-3-642-38209-3_3 Kevin Falzon and Gordon J. Pace. 2012. Combining testing and runtime verification techniques. In Proceedings of the 8th International Workshop Model-Based Methodologies for Pervasive and Embedded Software (MOMPES\u201912), Ricardo Jorge Machado, Rita Suzana Pitangueira Maciel, Julia Rubin, and Goetz Botterweck (Eds.), Lecture Notes in Computer Science,Vol. 7706. Springer, 38--57. DOI:https:\/\/doi.org\/10.1007\/978-3-642-38209-3_3"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2018.11.008"},{"key":"e_1_2_1_49_1","volume-title":"Proceedings of the 2018 International Conference on Autonomous Agents and Multiagent Systems (AAMAS\u201918)","author":"Ferrando Angelo","year":"2018","unstructured":"Angelo Ferrando , Louise A. Dennis , Davide Ancona , Michael Fisher , and Viviana Mascardi . 2018 . Recognising assumption violations in autonomous systems verification . In Proceedings of the 2018 International Conference on Autonomous Agents and Multiagent Systems (AAMAS\u201918) . Angelo Ferrando, Louise A. Dennis, Davide Ancona, Michael Fisher, and Viviana Mascardi. 2018. Recognising assumption violations in autonomous systems verification. In Proceedings of the 2018 International Conference on Autonomous Agents and Multiagent Systems (AAMAS\u201918)."},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the 2018 International Conference on Autonomous Agents and Multiagent Systems (AAMAS\u201918)","author":"Ferrando Angelo","year":"2018","unstructured":"Angelo Ferrando , Louise A. Dennis , Davide Ancona , Michael Fisher , and Viviana Mascardi . 2018 . Recognising assumption violations in autonomous systems verification . In Proceedings of the 2018 International Conference on Autonomous Agents and Multiagent Systems (AAMAS\u201918) . ACM, 1933--1935. Angelo Ferrando, Louise A. Dennis, Davide Ancona, Michael Fisher, and Viviana Mascardi. 2018. Recognising assumption violations in autonomous systems verification. In Proceedings of the 2018 International Conference on Autonomous Agents and Multiagent Systems (AAMAS\u201918). ACM, 1933--1935."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03769-7_15"},{"key":"e_1_2_1_52_1","volume-title":"Bernd-Holger Schlingloff, Michael Winikoff, and Neil Yorke-Smith.","author":"Fisher Michael","year":"2020","unstructured":"Michael Fisher , Viviana Mascardi , Kristin Yvonne Rozier , Bernd-Holger Schlingloff, Michael Winikoff, and Neil Yorke-Smith. 2020 . Towards a framework for certification of reliable autonomous systems. arxiv:2001.09124. https:\/\/arxiv.org\/abs\/2001.09124. Michael Fisher, Viviana Mascardi, Kristin Yvonne Rozier, Bernd-Holger Schlingloff, Michael Winikoff, and Neil Yorke-Smith. 2020. Towards a framework for certification of reliable autonomous systems. arxiv:2001.09124. https:\/\/arxiv.org\/abs\/2001.09124."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3328433.3328462"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44429-7_2"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788803"},{"key":"e_1_2_1_56_1","volume-title":"Proceedings of the REX Workshop on Real-Time: Theory in Practice","author":"Henzinger Thomas A.","unstructured":"Thomas A. Henzinger , Zohar Manna , and Amir Pnueli . 1991. Timed transition systems . In Proceedings of the REX Workshop on Real-Time: Theory in Practice , J. W. de Bakker, Cornelis Huizing, Willem P. de Roever, and Grzegorz Rozenberg (Eds.), Lecture Notes in Computer Science, Vol. 600 . Springer , 226--251. DOI:https:\/\/doi.org\/10.1007\/BFb0031995 10.1007\/BFb0031995 Thomas A. Henzinger, Zohar Manna, and Amir Pnueli. 1991. Timed transition systems. In Proceedings of the REX Workshop on Real-Time: Theory in Practice, J. W. de Bakker, Cornelis Huizing, Willem P. de Roever, and Grzegorz Rozenberg (Eds.), Lecture Notes in Computer Science, Vol. 600. Springer, 226--251. DOI:https:\/\/doi.org\/10.1007\/BFb0031995"},{"key":"e_1_2_1_57_1","volume-title":"Zuck","author":"Hinrichs Timothy L.","year":"2014","unstructured":"Timothy L. Hinrichs , A. Prasad Sistla , and Lenore D . Zuck . 2014 . Model check what you can, runtime verify the rest. In HOWARD-60: A Festschrift on the Occasion of Howard Barringer\u2019s 60th Birthday, Andrei Voronkov and Margarita V. Korovina (Eds.). EPiC Series in Computing, Vol. 42 . EasyChair , 234--244. https:\/\/easychair.org\/publications\/paper\/tq7. Timothy L. Hinrichs, A. Prasad Sistla, and Lenore D. Zuck. 2014. Model check what you can, runtime verify the rest. In HOWARD-60: A Festschrift on the Occasion of Howard Barringer\u2019s 60th Birthday, Andrei Voronkov and Margarita V. Korovina (Eds.). EPiC Series in Computing, Vol. 42. EasyChair, 234--244. https:\/\/easychair.org\/publications\/paper\/tq7."},{"key":"e_1_2_1_58_1","volume-title":"The SPIN Model Checker--Primer and Reference Manual","author":"Holzmann Gerard J.","unstructured":"Gerard J. Holzmann . 2004. The SPIN Model Checker--Primer and Reference Manual . Addison-Wesley . Gerard J. Holzmann. 2004. The SPIN Model Checker--Primer and Reference Manual. Addison-Wesley."},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2015.7353863"},{"key":"e_1_2_1_60_1","unstructured":"Industry Research. 2019. Software Testing Services Market by Product End-users and Geography\u2014Global Forecast and Analysis 2019-2023. Retrieved from https:\/\/www.industryresearch.co\/software-testing-services-market-by-product-end-users-and-geography-global-forecast-and-analysis-2019-2023-14620379.  Industry Research. 2019. Software Testing Services Market by Product End-users and Geography\u2014Global Forecast and Analysis 2019-2023. Retrieved from https:\/\/www.industryresearch.co\/software-testing-services-market-by-product-end-users-and-geography-global-forecast-and-analysis-2019-2023-14620379."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/IRC.2019.00059"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.05.006"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-67531-2_14"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"e_1_2_1_65_1","series-title":"Lecture Notes in Computer Science","volume-title":"Rozier","author":"Li Jianwen","year":"2018","unstructured":"Jianwen Li and Kristin Y . Rozier . 2018 . MLTL benchmark generation via formula progression. In Proceedings of the 18th International Conference on Runtime Verification (RV\u201918), Christian Colombo and Martin Leucker (Eds.), Lecture Notes in Computer Science , Vol. 11237 . Springer , 426--433. DOI:https:\/\/doi.org\/10.1007\/978-3-030-03769-7_25 10.1007\/978-3-030-03769-7_25 Jianwen Li and Kristin Y. Rozier. 2018. MLTL benchmark generation via formula progression. In Proceedings of the 18th International Conference on Runtime Verification (RV\u201918), Christian Colombo and Martin Leucker (Eds.), Lecture Notes in Computer Science, Vol. 11237. Springer, 426--433. DOI:https:\/\/doi.org\/10.1007\/978-3-030-03769-7_25"},{"key":"e_1_2_1_66_1","series-title":"Lecture Notes in Computer Science","volume-title":"Rozier","author":"Li Jianwen","year":"2019","unstructured":"Jianwen Li , Moshe Y. Vardi , and Kristin Y . Rozier . 2019 . Satisfiability checking for mission-time LTL. In Proceedings of the 31st International Conference on Computer Aided Verification (CAV\u201919)(), Isil Dillig and Serdar Tasiran (Eds.), Lecture Notes in Computer Science , Vol. 11562 . Springer , 3--22. DOI:https:\/\/doi.org\/10.1007\/978-3-030-25543-5_1 10.1007\/978-3-030-25543-5_1 Jianwen Li, Moshe Y. Vardi, and Kristin Y. Rozier. 2019. Satisfiability checking for mission-time LTL. In Proceedings of the 31st International Conference on Computer Aided Verification (CAV\u201919)(), Isil Dillig and Serdar Tasiran (Eds.), Lecture Notes in Computer Science, Vol. 11562. Springer, 3--22. DOI:https:\/\/doi.org\/10.1007\/978-3-030-25543-5_1"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_31"},{"key":"e_1_2_1_68_1","volume-title":"Automated Theorem Proving: A Logical Basis","author":"Loveland Donald W.","unstructured":"Donald W. Loveland . 2016. Automated Theorem Proving: A Logical Basis . Elsevier . Donald W. Loveland. 2016. Automated Theorem Proving: A Logical Basis. Elsevier."},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"e_1_2_1_71_1","volume-title":"Proceedings of the ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/SIGSOFT FSE\u201919)","author":"Menghi Claudio","unstructured":"Claudio Menghi , Shiva Nejati , Khouloud Gaaloul , and Lionel C. Briand . 2019. Generating automated and online test oracles for Simulink models with continuous and uncertain behaviors . In Proceedings of the ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/SIGSOFT FSE\u201919) , Marlon Dumas, Dietmar Pfahl, Sven Apel, and Alessandra Russo (Eds.). ACM, 27--38. DOI:https:\/\/doi.org\/10.1145\/3338906.3338920 10.1145\/3338906.3338920 Claudio Menghi, Shiva Nejati, Khouloud Gaaloul, and Lionel C. Briand. 2019. Generating automated and online test oracles for Simulink models with continuous and uncertain behaviors. In Proceedings of the ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/SIGSOFT FSE\u201919), Marlon Dumas, Dietmar Pfahl, Sven Apel, and Alessandra Russo (Eds.). ACM, 27--38. DOI:https:\/\/doi.org\/10.1145\/3338906.3338920"},{"key":"#cr-split#-e_1_2_1_72_1.1","doi-asserted-by":"crossref","unstructured":"Giorgio Metta and Angelo Cangelosi. 2012. Cognitive Robotics. Springer US Boston MA 613--616. DOI:https:\/\/doi.org\/10.1007\/978-1-4419-1428-6_654 10.1007\/978-1-4419-1428-6_654","DOI":"10.1007\/978-1-4419-1428-6_654"},{"key":"#cr-split#-e_1_2_1_72_1.2","doi-asserted-by":"crossref","unstructured":"Giorgio Metta and Angelo Cangelosi. 2012. Cognitive Robotics. Springer US Boston MA 613--616. DOI:https:\/\/doi.org\/10.1007\/978-1-4419-1428-6_654","DOI":"10.1007\/978-1-4419-1428-6_654"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2018.2859946"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/s12559-012-9129-4"},{"key":"e_1_2_1_75_1","volume-title":"Proceedings of the 6th International Conference on Runtime Verification (RV\u201915)","author":"Nguyen Luan Viet","unstructured":"Luan Viet Nguyen , Christian Schilling , Sergiy Bogomolov , and Taylor T. Johnson . 2015. Runtime verification for hybrid analysis tools . In Proceedings of the 6th International Conference on Runtime Verification (RV\u201915) . Lecture Notes in Computer Science, 281--286. Luan Viet Nguyen, Christian Schilling, Sergiy Bogomolov, and Taylor T. Johnson. 2015. Runtime verification for hybrid analysis tools. In Proceedings of the 6th International Conference on Runtime Verification (RV\u201915). Lecture Notes in Computer Science, 281--286."},{"key":"#cr-split#-e_1_2_1_76_1.1","doi-asserted-by":"crossref","unstructured":"Dejan Nickovic Olivier Lebeltel Oded Maler Thomas Ferr\u00e8re and Dogan Ulus. 2018. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. In Proceedings of the 24th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18) Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS'18) Dirk Beyer and Marieke Huisman (Eds.) Vol. 10806. Springer 303--319. DOI:https:\/\/doi.org\/10.1007\/978-3-319-89963-3_18 10.1007\/978-3-319-89963-3_18","DOI":"10.1007\/978-3-319-89963-3_18"},{"key":"#cr-split#-e_1_2_1_76_1.2","doi-asserted-by":"crossref","unstructured":"Dejan Nickovic Olivier Lebeltel Oded Maler Thomas Ferr\u00e8re and Dogan Ulus. 2018. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. In Proceedings of the 24th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18) Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS'18) Dirk Beyer and Marieke Huisman (Eds.) Vol. 10806. Springer 303--319. DOI:https:\/\/doi.org\/10.1007\/978-3-319-89963-3_18","DOI":"10.1007\/978-3-319-89963-3_18"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85778-5_1"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337364"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1147\/sj.462.0265"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_81_1","volume-title":"Current Trends in Concurrency, Overviews and Tutorials","author":"Pnueli Amir","unstructured":"Amir Pnueli . 1986. Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends . In Current Trends in Concurrency, Overviews and Tutorials , J. W. de Bakker, Willem P. de Roever, and Grzegorz Rozenberg (Eds.). Lecture Notes in Computer Science, Vol. 224 . Springer , 510--584. DOI:https:\/\/doi.org\/10.1007\/BFb0027047 10.1007\/BFb0027047 Amir Pnueli. 1986. Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. In Current Trends in Concurrency, Overviews and Tutorials, J. W. de Bakker, Willem P. de Roever, and Grzegorz Rozenberg (Eds.). Lecture Notes in Computer Science, Vol. 224. Springer, 510--584. DOI:https:\/\/doi.org\/10.1007\/BFb0027047"},{"key":"e_1_2_1_82_1","volume-title":"Jadex: A BDI reasoning engine. In Multi-Agent Programming: Languages, Platforms and Applications. Multiagent Systems, Artificial Societies, and Simulated Organizations","author":"Pokahr Alexander","year":"2005","unstructured":"Alexander Pokahr , Lars Braubach , and Winfried Lamersdorf . 2005 . Jadex: A BDI reasoning engine. In Multi-Agent Programming: Languages, Platforms and Applications. Multiagent Systems, Artificial Societies, and Simulated Organizations , Vol. 15 . Springer , 149--174. Alexander Pokahr, Lars Braubach, and Winfried Lamersdorf. 2005. Jadex: A BDI reasoning engine. In Multi-Agent Programming: Languages, Platforms and Applications. Multiagent Systems, Artificial Societies, and Simulated Organizations, Vol. 15. Springer, 149--174."},{"key":"e_1_2_1_83_1","volume-title":"Proceedings of the Workshop on Open Source Software. IEEE, Japan.","author":"Quigley Morgan","year":"2009","unstructured":"Morgan Quigley , Ken Conley , Brian Gerkey , Josh Faust , Tully Foote , Jeremy Leibs , Rob Wheeler , and Andrew Ng . 2009 . ROS: An open-source robot operating system . In Proceedings of the Workshop on Open Source Software. IEEE, Japan. Morgan Quigley, Ken Conley, Brian Gerkey, Josh Faust, Tully Foote, Jeremy Leibs, Rob Wheeler, and Andrew Ng. 2009. ROS: An open-source robot operating system. In Proceedings of the Workshop on Open Source Software. IEEE, Japan."},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.12.010"},{"key":"e_1_2_1_85_1","volume-title":"Agents Breaking Away: Proceedings of the 7th European Workshop on Modelling Autonomous Agents in a Multi-Agent World (MAAMAW\u201996)","author":"Rao Anand S.","unstructured":"Anand S. Rao . 1996. AgentSpeak(L): BDI agents speak out in a logical computable language . In Agents Breaking Away: Proceedings of the 7th European Workshop on Modelling Autonomous Agents in a Multi-Agent World (MAAMAW\u201996) . 42--55. Anand S. Rao. 1996. AgentSpeak(L): BDI agents speak out in a logical computable language. In Agents Breaking Away: Proceedings of the 7th European Workshop on Modelling Autonomous Agents in a Multi-Agent World (MAAMAW\u201996). 42--55."},{"key":"e_1_2_1_86_1","volume-title":"Proceedings of the 1st International Conference Multi-Agent Systems (ICMAS\u201995)","author":"Rao A. S.","unstructured":"A. S. Rao and M. Georgeff . 1995. BDI agents: From theory to practice . In Proceedings of the 1st International Conference Multi-Agent Systems (ICMAS\u201995) . San Francisco, CA, 312--319. A. S. Rao and M. Georgeff. 1995. BDI agents: From theory to practice. In Proceedings of the 1st International Conference Multi-Agent Systems (ICMAS\u201995). San Francisco, CA, 312--319."},{"key":"e_1_2_1_87_1","volume-title":"Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR&R\u201991)","author":"Rao A. S.","unstructured":"A. S. Rao and M. P. Georgeff . 1991. Modeling Agents within a BDI-Architecture . In Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR&R\u201991) . 473--484. A. S. Rao and M. P. Georgeff. 1991. Modeling Agents within a BDI-Architecture. In Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR&R\u201991). 473--484."},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29860-8_21"},{"key":"e_1_2_1_90_1","volume-title":"Proceedings of the 24th International Conference on Software Engineering (ICSE\u201902)","author":"Smith Rachel L.","unstructured":"Rachel L. Smith , George S. Avrunin , Lori A. Clarke , and Leon J. Osterweil . 2002. PROPEL: An approach supporting property elucidation . In Proceedings of the 24th International Conference on Software Engineering (ICSE\u201902) , Will Tracz, Michal Young, and Jeff Magee (Eds.). ACM, 11--21. DOI:https:\/\/doi.org\/10.1145\/581339.581345 10.1145\/581339.581345 Rachel L. Smith, George S. Avrunin, Lori A. Clarke, and Leon J. Osterweil. 2002. PROPEL: An approach supporting property elucidation. In Proceedings of the 24th International Conference on Software Engineering (ICSE\u201902), Will Tracz, Michal Young, and Jeff Magee (Eds.). ACM, 11--21. DOI:https:\/\/doi.org\/10.1145\/581339.581345"},{"key":"e_1_2_1_91_1","volume-title":"Proceedings of the 18th IEEE International Conference on Automated Software Engineering (ASE\u201903)","author":"Tkachuk Oksana","unstructured":"Oksana Tkachuk , Matthew B. Dwyer , and Corina S. Pasareanu . 2003. Automated environment generation for software model checking . In Proceedings of the 18th IEEE International Conference on Automated Software Engineering (ASE\u201903) . 116--129. Oksana Tkachuk, Matthew B. Dwyer, and Corina S. Pasareanu. 2003. Automated environment generation for software model checking. In Proceedings of the 18th IEEE International Conference on Automated Software Engineering (ASE\u201903). 116--129."},{"key":"e_1_2_1_92_1","doi-asserted-by":"crossref","unstructured":"Paolo Torroni Pinar Yolum Munindar P. Singh Marco Alberti Federico Chesani Marco Gavanelli Evelina Lamma and Paola Mello. 2009. Modelling interactions via commitments and expectations. In Handbook of Research on Multi-Agent Systems: Semantics and Dynamics of Organizational Models. IGI Global.  Paolo Torroni Pinar Yolum Munindar P. Singh Marco Alberti Federico Chesani Marco Gavanelli Evelina Lamma and Paola Mello. 2009. Modelling interactions via commitments and expectations. In Handbook of Research on Multi-Agent Systems: Semantics and Dynamics of Organizational Models. IGI Global.","DOI":"10.4018\/978-1-60566-256-5.ch011"},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2019.2937471"},{"key":"e_1_2_1_94_1","unstructured":"Markus Vincze and David Vernon. 2017. Industrial Priorities for Cognitive Robotics Deliverable D-3.1 RockEU2--Robotics Coordination Action for Europe Two.  Markus Vincze and David Vernon. 2017. Industrial Priorities for Cognitive Robotics Deliverable D-3.1 RockEU2--Robotics Coordination Action for Europe Two."},{"key":"e_1_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2004.831197"},{"key":"e_1_2_1_96_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0269888900008122"},{"key":"e_1_2_1_97_1","volume-title":"Proceedings of the 9th International Conference on Quality Software (QSIC\u201909)","author":"Daniel","year":"2009","unstructured":"Daniel M. Zimmerman and Joseph R. Kiniry. 2009. A verification-centric software development process for Java . In Proceedings of the 9th International Conference on Quality Software (QSIC\u201909) , Byoungju Choi (Ed.). IEEE Computer Society, 76--85. DOI:https:\/\/doi.org\/10.1109\/QSIC. 2009 .18 10.1109\/QSIC.2009.18 Daniel M. Zimmerman and Joseph R. Kiniry. 2009. A verification-centric software development process for Java. In Proceedings of the 9th International Conference on Quality Software (QSIC\u201909), Byoungju Choi (Ed.). IEEE Computer Society, 76--85. DOI:https:\/\/doi.org\/10.1109\/QSIC.2009.18"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3447246","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3447246","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:27Z","timestamp":1750195707000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3447246"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,5,10]]},"references-count":96,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,10,31]]}},"alternative-id":["10.1145\/3447246"],"URL":"https:\/\/doi.org\/10.1145\/3447246","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,5,10]]},"assertion":[{"value":"2020-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-05-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}