{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T15:24:38Z","timestamp":1790522678850,"version":"4.1.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319989372","type":"print"},{"value":"9783319989389","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-98938-9_10","type":"book-chapter","created":{"date-parts":[[2018,8,8]],"date-time":"2018-08-08T11:08:34Z","timestamp":1533726514000},"page":"161-171","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":44,"title":["Robotics and Integrated Formal Methods: Necessity Meets Opportunity"],"prefix":"10.1007","author":[{"given":"Marie","family":"Farrell","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matt","family":"Luckcuck","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,8,9]]},"reference":[{"issue":"1","key":"10_CR1","first-page":"35","volume":"117","author":"N Akhtar","year":"2014","unstructured":"Akhtar, N.: Contribution to the formal specification and verification of a multi-agent robotic system. Eur. J. Sci. Res. 117(1), 35\u201355 (2014)","journal-title":"Eur. J. Sci. Res."},{"key":"10_CR2","doi-asserted-by":"publisher","first-page":"79","DOI":"10.4204\/EPTCS.232.10","volume":"232","author":"A Aniculaesei","year":"2016","unstructured":"Aniculaesei, A., Arnsberger, D., Howar, F., Rausch, A.: Towards the verification of safety-critical autonomous systems in dynamic environments. Electron. Proc. Theor. Comput. Sci. 232, 79\u201390 (2016)","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-319-22416-9_4","volume-title":"Towards Autonomous Robotic Systems","author":"L Antu\u00f1a","year":"2015","unstructured":"Antu\u00f1a, L., Araiza-Illan, D., Campos, S., Eder, K.: Symmetry reduction enables model checking of more complex emergent behaviours of swarm navigation algorithms. In: Dixon, C., Tuyls, K. (eds.) TAROS 2015. LNCS (LNAI), vol. 9287, pp. 26\u201337. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22416-9_4"},{"issue":"11\u201312","key":"10_CR4","doi-asserted-by":"publisher","first-page":"1227","DOI":"10.1007\/s00170-007-1288-1","volume":"39","author":"ZM Bi","year":"2008","unstructured":"Bi, Z.M., Lang, S.Y.T., Verner, M., Orban, P.: Development of reconfigurable machines. Int. J. Adv. Manuf. Technol. 39(11\u201312), 1227\u20131251 (2008)","journal-title":"Int. J. Adv. Manuf. Technol."},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Braman, J.M.B., Murray, R.M., Wagner, D.A.: Safety verification of a fault tolerant reconfigurable autonomous goal-based robotic control system. In: International Conference on Intelligent Robots and Systems, pp. 853\u2013858. IEEE (2007)","DOI":"10.1109\/IROS.2007.4399230"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-319-08915-7_4","volume-title":"Models@run.time","author":"BHC Cheng","year":"2014","unstructured":"Cheng, B.H.C., et al.: Using models at runtime to address assurance for self-adaptive systems. In: Bencomo, N., France, R., Cheng, B.H.C., A\u00dfmann, U. (eds.) Models@run.time. LNCS, vol. 8378, pp. 101\u2013136. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08915-7_4"},{"issue":"4","key":"10_CR7","doi-asserted-by":"publisher","first-page":"634","DOI":"10.1080\/00207721.2013.793890","volume":"46","author":"J Choi","year":"2015","unstructured":"Choi, J., Kim, S., Tsourdos, A.: Verification of heterogeneous multi-agent system using MCMAS. Int. J. Syst. Sci. 46(4), 634\u2013651 (2015)","journal-title":"Int. J. Syst. Sci."},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-03240-0_11","volume-title":"Formal Methods for Industrial Critical Systems","author":"S Colin","year":"2009","unstructured":"Colin, S., Lanoix, A., Kouchnarenko, O., Souqui\u00e8res, J.: Using CSP$$\\vert \\vert $$B components: application to a platoon of vehicles. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 103\u2013118. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03240-0_11"},{"issue":"4","key":"10_CR9","doi-asserted-by":"publisher","first-page":"830","DOI":"10.1109\/TR.2014.2335995","volume":"63","author":"E Denney","year":"2014","unstructured":"Denney, E., Pai, G.: Automating the assembly of aviation safety cases. IEEE Trans. Reliab. 63(4), 830\u2013849 (2014)","journal-title":"IEEE Trans. Reliab."},{"issue":"1","key":"10_CR10","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10515-011-0088-x","volume":"19","author":"LA Dennis","year":"2012","unstructured":"Dennis, L.A., Fisher, M., Webster, M., Bordini, R.H.: Model checking agent programming languages. Autom. Softw. Eng. 19(1), 5\u201363 (2012)","journal-title":"Autom. Softw. Eng."},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-319-67531-2_11","volume-title":"Runtime Verification","author":"A Desai","year":"2017","unstructured":"Desai, A., Dreossi, T., Seshia, S.A.: Combining model checking and runtime verification for safe robotics. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 172\u2013189. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-67531-2_11"},{"issue":"1\/2","key":"10_CR12","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/B:AGNT.0000019688.11109.19","volume":"9","author":"M D\u2019Inverno","year":"2004","unstructured":"D\u2019Inverno, M., Luck, M., Georgeff, M., Kinny, D., Wooldridge, M.: The dMARS architecture: a specification of the distributed multi-agent reasoning system. Auton. Agent. Multi. Agent. Syst. 9(1\/2), 5\u201353 (2004)","journal-title":"Auton. Agent. Multi. Agent. Syst."},{"issue":"9","key":"10_CR13","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/2500468.2494558","volume":"56","author":"M Fisher","year":"2013","unstructured":"Fisher, M., Dennis, L.A., Webster, M.: Verifying autonomous systems. Commun. ACM 56(9), 84\u201393 (2013)","journal-title":"Commun. ACM"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Hinchey, M.G., Rouff, C.A., Rash, J.L., Truszkowski, W.F.: Requirements of an integrated formal method for intelligent swarms. In: Formal Methods for Industrial Critical Systems, pp. 125\u2013133. ACM Press (2005)","DOI":"10.1145\/1081180.1081196"},{"issue":"1","key":"10_CR15","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/s10458-008-9065-6","volume":"19","author":"KV Hindriks","year":"2009","unstructured":"Hindriks, K.V., Meyer, J.-J.C.: Toward a programming theory for rational agents. Auton. Agent. Multi. Agent. Syst. 19(1), 4\u201329 (2009)","journal-title":"Auton. Agent. Multi. Agent. Syst."},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Izzo, P., Qu, H., Veres, S.M.: A stochastically verifiable autonomous control architecture with reasoning. In: IEEE Conference on Decision and Control, pp. 4985\u20134991 (2016)","DOI":"10.1109\/CDC.2016.7799031"},{"key":"10_CR17","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1016\/j.scico.2017.05.006","volume":"148","author":"M Kamali","year":"2017","unstructured":"Kamali, M., Dennis, L.A., McAree, O., Fisher, M., Veres, S.M.: Formal verification of autonomous vehicle platooning. Sci. Comput. Program. 148, 88\u2013106 (2017)","journal-title":"Sci. Comput. Program."},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Kamali, M., Linker, S., Fisher, M.: Modular verification of vehicle platooning with respect to decisions, space and time. arXiv preprint arXiv:1804.06647 (2018)","DOI":"10.1007\/978-3-030-12988-0_2"},{"issue":"2","key":"10_CR19","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/j.robot.2011.10.005","volume":"60","author":"S Konur","year":"2012","unstructured":"Konur, S., Dixon, C., Fisher, M.: Analysing robot swarm behaviour via probabilistic model checking. Robot. Auton. Syst. 60(2), 199\u2013213 (2012)","journal-title":"Robot. Auton. Syst."},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-319-33600-8_13","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"F Kossak","year":"2016","unstructured":"Kossak, F., Mashkoor, A.: How to select the suitable formal method for\u00a0an industrial application: a survey. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 213\u2013228. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33600-8_13"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-319-10506-2_18","volume-title":"Computer Safety, Reliability, and Security","author":"M Machin","year":"2014","unstructured":"Machin, M., Dufoss\u00e9, F., Blanquart, J.-P., Guiochet, J., Powell, D., Waeselynck, H.: Specifying safety monitors for autonomous systems using model-checking. In: Bondavalli, A., Di Giandomenico, F. (eds.) SAFECOMP 2014. LNCS, vol. 8666, pp. 262\u2013277. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10506-2_18"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Mitsch, S., Ghorbal, K., Platzer, A.: On provably safe obstacle avoidance for autonomous robotic ground vehicles. In: Robotics and Science and Systems (2013)","DOI":"10.15607\/RSS.2013.IX.014"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Moarref, S., Kress-Gazit, H.: Decentralized control of robotic swarms from high-level temporal logic specifications. In: International Symposium on Multi-robot and Multi-agent Systems. IEEE (2017)","DOI":"10.1109\/MRS.2017.8250926"},{"key":"10_CR24","unstructured":"Morse, J., Araiza-Illan, D., Lawry, J., Richards, A., Eder, K.: Formal specification and analysis of autonomous systems under partial compliance. arXiv preprint arXiv:1603.01082 (2016)"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-319-23820-3_13","volume-title":"Runtime Verification","author":"D Phan","year":"2015","unstructured":"Phan, D., Yang, J., Ratasich, D., Grosu, R., Smolka, S.A., Stoller, S.D.: Collision avoidance for mobile robots with limited sensing and limited information about the environment. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 201\u2013215. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23820-3_13"},{"key":"10_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/978-3-540-73210-5_26","volume-title":"Integrated Formal Methods","author":"R Podorozhny","year":"2007","unstructured":"Podorozhny, R., Khurshid, S., Perry, D., Zhang, X.: Verification of multi-agent negotiations using the alloy analyzer. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 501\u2013517. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73210-5_26"},{"key":"10_CR27","unstructured":"Quigley, M., et al.: ROS: an open-source robot operating system. In: ICRA Workshop on Open Source Software, vol. 3, p. 5 (2009)"},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-319-66845-1_2","volume-title":"Integrated Formal Methods","author":"P Ribeiro","year":"2017","unstructured":"Ribeiro, P., Miyazawa, A., Li, W., Cavalcanti, A., Timmis, J.: Modelling and verification of timed robotic controllers. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 18\u201333. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_2"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-319-66845-1_4","volume-title":"Integrated Formal Methods","author":"A Rizaldi","year":"2017","unstructured":"Rizaldi, A., et al.: Formalising and monitoring traffic rules for autonomous vehicles in Isabelle\/HOL. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 50\u201366. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_4"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Simmons, R., Pecheur, C., Srinivasan, G.: Towards automatic verification of autonomous systems. In: International Conference on Intelligent Robots and Systems, vol. 2, pp. 1410\u20131415. IEEE (2000)","DOI":"10.1109\/IROS.2000.893218"},{"key":"10_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-662-43652-3_6","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"G Smith","year":"2014","unstructured":"Smith, G., Li, Q.: MAZE: an extension of Object-Z for multi-agent systems. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 72\u201385. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43652-3_6"},{"key":"10_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-642-33678-2_18","volume-title":"Computer Safety, Reliability, and Security","author":"A Tarasyuk","year":"2012","unstructured":"Tarasyuk, A., Pereverzeva, I., Troubitsyna, E., Latvala, T., Nummila, L.: Formal development and assessment of a reconfigurable on-board satellite system. In: Ortmeier, F., Daniel, P. (eds.) SAFECOMP 2012. LNCS, vol. 7612, pp. 210\u2013222. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33678-2_18"},{"issue":"5","key":"10_CR33","first-page":"258","volume":"11","author":"M Webster","year":"2014","unstructured":"Webster, M., Cameron, N., Fisher, M., Jump, M.: Generating certification evidence for autonomous unmanned aircraft using model checking and simulation. J. Aerosp. Inf. Syst. 11(5), 258\u2013279 (2014)","journal-title":"J. Aerosp. Inf. Syst."},{"issue":"2","key":"10_CR34","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1109\/THMS.2015.2425139","volume":"46","author":"M Webster","year":"2016","unstructured":"Webster, M., et al.: Toward reliable autonomous robotic assistants through formal verification: a case study. IEEE Trans. Hum.-Mach. Syst. 46(2), 186\u2013196 (2016)","journal-title":"IEEE Trans. Hum.-Mach. Syst."},{"key":"10_CR35","unstructured":"Webster, M., et al.: An assurance-based approach to verification and validation of human-robot teams. arXiv preprint arXiv:1608.07403 (2016)"},{"key":"10_CR36","doi-asserted-by":"crossref","unstructured":"Weyns, D., Iftikhar, M.U., de la Iglesia, D.G., Ahmad, T.: A survey of formal methods in self-adaptive systems. In: International C* Conference on Computer Science and Software Engineering, pp. 67\u201379. ACM (2012)","DOI":"10.1145\/2347583.2347592"},{"key":"10_CR37","doi-asserted-by":"crossref","unstructured":"Weyns, D., Malek, S.: FORMS: a formal reference model for self-adaptation. In: International Conference on Autonomic Computing, pp. 205\u2013214. ACM (2010)","DOI":"10.1145\/1809049.1809078"},{"issue":"4","key":"10_CR38","doi-asserted-by":"publisher","first-page":"363","DOI":"10.5772\/5769","volume":"2","author":"AF Winfield","year":"2005","unstructured":"Winfield, A.F., Sa, J., Gago, M.C.F., Dixon, C., Fisher, M.: On formal specification of emergent behaviours in swarm robotic systems. Int. J. Adv. Robot. Syst. 2(4), 363\u2013370 (2005)","journal-title":"Int. J. Adv. Robot. Syst."}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-98938-9_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,21]],"date-time":"2019-10-21T21:01:35Z","timestamp":1571691695000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-98938-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319989372","9783319989389"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-98938-9_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}