{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,21]],"date-time":"2025-08-21T17:57:32Z","timestamp":1755799052017,"version":"3.44.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783032014856"},{"type":"electronic","value":"9783032014863"}],"license":[{"start":{"date-parts":[[2025,8,13]],"date-time":"2025-08-13T00:00:00Z","timestamp":1755043200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,13]],"date-time":"2025-08-13T00:00:00Z","timestamp":1755043200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-01486-3_21","type":"book-chapter","created":{"date-parts":[[2025,8,19]],"date-time":"2025-08-19T15:47:01Z","timestamp":1755618421000},"page":"259-272","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Varanus: Runtime Verification for\u00a0CSP"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6444-9312","authenticated-orcid":false,"given":"Matt","family":"Luckcuck","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8711-4670","authenticated-orcid":false,"given":"Angelo","family":"Ferrando","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6928-0176","authenticated-orcid":false,"given":"Fatma","family":"Faruq","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,8,13]]},"reference":[{"key":"21_CR1","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2021.102610","volume":"205","author":"D Ancona","year":"2021","unstructured":"Ancona, D., Franceschini, L., Ferrando, A., Mascardi, V.: RML: theory and practice of a domain specific language for runtime verification. Sci. Comput. Program. 205, 102610 (2021). https:\/\/doi.org\/10.1016\/J.SCICO.2021.102610","journal-title":"Sci. Comput. Program."},{"issue":"11","key":"21_CR2","doi-asserted-by":"publisher","first-page":"365","DOI":"10.2514\/1.49356","volume":"7","author":"H Barringer","year":"2010","unstructured":"Barringer, H., Groce, A., Havelund, K., Smith, M.H.: Formal analysis of log files. J. Aerosp. Comput. Inf. Commun. 7(11), 365\u2013390 (2010). https:\/\/doi.org\/10.2514\/1.49356","journal-title":"J. Aerosp. Comput. Inf. Commun."},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-642-21437-0_7","volume-title":"FM 2011: Formal Methods","author":"H Barringer","year":"2011","unstructured":"Barringer, H., Havelund, K.: TraceContract: a scala DSL for trace analysis. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 57\u201372. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_7"},{"issue":"2","key":"21_CR4","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/S1571-0661(04)00247-6","volume":"55","author":"D Bartetzko","year":"2001","unstructured":"Bartetzko, D., Fischer, C., M\u00f6ller, M., Wehrheim, H.: Jass \u2013 java with assertions. Electron. Notes Theor. Comput. Sci. 55(2), 103\u2013117 (2001). https:\/\/doi.org\/10.1016\/S1571-0661(04)00247-6","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"3","key":"21_CR5","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1109\/MS.2011.27","volume":"28","author":"A Basu","year":"2011","unstructured":"Basu, A., et al.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28(3), 41\u201348 (2011). https:\/\/doi.org\/10.1109\/MS.2011.27","journal-title":"IEEE Softw."},{"key":"21_CR6","doi-asserted-by":"publisher","first-page":"631","DOI":"10.3233\/978-1-58603-891-5-631","volume":"178","author":"A Basu","year":"2008","unstructured":"Basu, A., et al.: Incremental component-based construction and verification of a robotic system. Front. Artif. Intell. Appl. 178, 631\u2013635 (2008). https:\/\/doi.org\/10.3233\/978-1-58603-891-5-631","journal-title":"Front. Artif. Intell. Appl."},{"issue":"1","key":"21_CR7","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1109\/MRA.2008.931631","volume":"16","author":"S Bensalem","year":"2009","unstructured":"Bensalem, S., Gallien, M., Ingrand, F., Kahloul, I., Thanh-Hung, N.: Designing autonomous robots. IEEE Robot. Autom. Mag. 16(1), 67\u201377 (2009). https:\/\/doi.org\/10.1109\/MRA.2008.931631","journal-title":"IEEE Robot. Autom. Mag."},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/978-3-319-25150-9_29","volume-title":"Theoretical Aspects of Computing - ICTAC 2015","author":"A Cavalcanti","year":"2015","unstructured":"Cavalcanti, A., Huang, W., Peleska, J., Woodcock, J.: CSP and Kripke structures. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 505\u2013523. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25150-9_29"},{"key":"21_CR9","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., et al.: From spot 2.0 to spot 2.10: what\u2019s new? In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, 7\u201310 August 2022, Proceedings, Part II. LNCS, vol. 13372, pp. 174\u2013187. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-642-24690-6_15","volume-title":"Software Engineering and Formal Methods","author":"Y Falcone","year":"2011","unstructured":"Falcone, Y., Jaber, M., Nguyen, T.-H., Bozga, M., Bensalem, S.: Runtime verification of component-based systems. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 204\u2013220. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24690-6_15"},{"issue":"1","key":"21_CR11","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/S10703-022-00395-7","volume":"59","author":"A Ferrando","year":"2021","unstructured":"Ferrando, A., et al.: Bridging the gap between single- and multi-model predictive runtime verification. Formal Methods Syst. Des. 59(1), 44\u201376 (2021). https:\/\/doi.org\/10.1007\/S10703-022-00395-7","journal-title":"Formal Methods Syst. Des."},{"key":"21_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-030-63486-5_40","volume-title":"Towards Autonomous Robotic Systems","author":"A Ferrando","year":"2020","unstructured":"Ferrando, A., Cardoso, R.C., Fisher, M., Ancona, D., Franceschini, L., Mascardi, V.: ROSMonitoring: a runtime verification framework for ROS. In: Mohammad, A., Dong, X., Russo, M. (eds.) TAROS 2020. LNCS (LNAI), vol. 12228, pp. 387\u2013399. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63486-5_40"},{"key":"21_CR13","doi-asserted-by":"publisher","unstructured":"Ferrando, A., Dennis, L.A., Cardoso, R.C., Fisher, M., Ancona, D., Mascardi, V.: Toward a holistic approach to verification and validation of autonomous cognitive systems. ACM Trans. Softw. Eng. Methodol. 30(4), 43:1\u201343:43 (2021). https:\/\/doi.org\/10.1145\/3447246","DOI":"10.1145\/3447246"},{"issue":"1","key":"21_CR14","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/0004-3702(82)90020-0","volume":"19","author":"C Forgy","year":"1982","unstructured":"Forgy, C.: Rete: a fast algorithm for the many patterns\/many objects match problem. Artif. Intell. 19(1), 17\u201337 (1982). https:\/\/doi.org\/10.1016\/0004-3702(82)90020-0","journal-title":"Artif. Intell."},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-54862-8_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Gibson-Robinson","year":"2014","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3\u2014a modern refinement checker for CSP. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187\u2013201. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_13"},{"issue":"2","key":"21_CR16","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/S10009-014-0309-2","volume":"17","author":"K Havelund","year":"2015","unstructured":"Havelund, K.: Rule-based runtime verification revisited. Int. J. Softw. Tools Technol. Transf. 17(2), 143\u2013170 (2015). https:\/\/doi.org\/10.1007\/S10009-014-0309-2","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/3-540-45251-6_6","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"M Leuschel","year":"2001","unstructured":"Leuschel, M., Currie, A., Massart, T.: How to make FDR spin LTL model checking of CSP by refinement. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 99\u2013118. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45251-6_6"},{"key":"21_CR18","doi-asserted-by":"publisher","unstructured":"Liu, S.B., Roehm, H., Heinzemann, C., Lutkebohle, I., Oehlerking, J., Althoff, M.: Provably safe motion of mobile robots in human environments. In: 2017 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS). IEEE (2017). https:\/\/doi.org\/10.1109\/iros.2017.8202313","DOI":"10.1109\/iros.2017.8202313"},{"key":"21_CR19","doi-asserted-by":"publisher","unstructured":"Luckcuck, M.: Using formal methods for autonomous systems: five recipes for formal verification. Proc. Inst. Mech. Engineers Part O: J. Risk Reliabil. (2021). https:\/\/doi.org\/10.1177\/1748006X211034970","DOI":"10.1177\/1748006X211034970"},{"issue":"5","key":"21_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3342355","volume":"52","author":"M Luckcuck","year":"2019","unstructured":"Luckcuck, M., Farrell, M., Dennis, L.A., Dixon, C., Fisher, M.: Formal specification and verification of autonomous robotic systems: a survey. ACM Comput. Surv. 52(5), 1\u201341 (2019). https:\/\/doi.org\/10.1145\/3342355","journal-title":"ACM Comput. Surv."},{"key":"21_CR21","unstructured":"Luckcuck, M., Farrell, M., Ferrando, A., Cardoso, R.C., Dennis, L.A., Fisher, M.: A compositional approach to verifying modular robotic systems (2023). https:\/\/arxiv.org\/abs\/2208.05507"},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-88808-6_2","volume-title":"Rule Representation, Interchange and Reasoning on the Web","author":"D Luckham","year":"2008","unstructured":"Luckham, D.: The power of events: an introduction to complex event processing in distributed enterprise systems. In: Bassiliades, N., Governatori, G., Paschke, A. (eds.) RuleML 2008. LNCS, vol. 5321, pp. 3\u20133. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88808-6_2"},{"issue":"2","key":"21_CR23","doi-asserted-by":"publisher","first-page":"62","DOI":"10.3390\/ROBOTICS12020062","volume":"12","author":"D MacConville","year":"2023","unstructured":"MacConville, D., Farrell, M., Luckcuck, M., Monahan, R.: Csp2turtle: verified turtle robot plans. Robotics 12(2), 62 (2023). https:\/\/doi.org\/10.3390\/ROBOTICS12020062","journal-title":"Robotics"},{"issue":"3","key":"21_CR24","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/S10009-011-0198-6","volume":"14","author":"PO Meredith","year":"2012","unstructured":"Meredith, P.O., Jin, D., Griffith, D., Chen, F., Rosu, G.: An overview of the MOP runtime verification framework. Int. J. Softw. Tools Technol. Transf. 14(3), 249\u2013289 (2012). https:\/\/doi.org\/10.1007\/S10009-011-0198-6","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"1\u20132","key":"21_CR25","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10703-016-0241-z","volume":"49","author":"S Mitsch","year":"2016","unstructured":"Mitsch, S., Platzer, A.: ModelPlex: verified runtime validation of verified cyberphysical system models. Formal Methods Syst. Des. 49(1\u20132), 33\u201374 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0241-z","journal-title":"Formal Methods Syst. Des."},{"issue":"5","key":"21_CR26","doi-asserted-by":"publisher","first-page":"3097","DOI":"10.1007\/s10270-018-00710-z","volume":"18","author":"A Miyazawa","year":"2019","unstructured":"Miyazawa, A., Ribeiro, P., Li, W., Cavalcanti, A., Timmis, J., Woodcock, J.: Robochart: modelling and verification of the functional behaviour of robotic applications. Softw. Syst. Model. 18(5), 3097\u20133149 (2019). https:\/\/doi.org\/10.1007\/s10270-018-00710-z","journal-title":"Softw. Syst. Model."},{"key":"21_CR27","unstructured":"Moller, M.: Specifying and checking java using CSP. In: Workshop on Formal Techniques for Java-like Programs, M\u00e1laga, Spain, p.\u00a09 (2002). http:\/\/www.cs.ru.nl\/ftfjp\/2002\/MichaelMoeller.pdf"},{"issue":"July","key":"21_CR28","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-319-11900-7_17","volume":"7","author":"A Nordmann","year":"2016","unstructured":"Nordmann, A., Hochgeschwender, N., Wigand, D., Wrede, S.: A survey on domain- specific languages in robotics. J. Softw. Eng. Robot. 7(July), 195\u2013206 (2016). https:\/\/doi.org\/10.1007\/978-3-319-11900-7_17","journal-title":"J. Softw. Eng. Robot."},{"key":"21_CR29","doi-asserted-by":"publisher","unstructured":"Pereira, A., Althoff, M.: Safety control of robots under computed torque control using reachable sets. In: 2015 IEEE International Conference on Robotics and Automation (ICRA). IEEE (2015). https:\/\/doi.org\/10.1109\/icra.2015.7139020","DOI":"10.1109\/icra.2015.7139020"},{"key":"21_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-319-48869-1_2","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"KY Rozier","year":"2016","unstructured":"Rozier, K.Y.: Specification: the biggest bottleneck in formal methods and autonomy. In: Blazy, S., Chechik, M. (eds.) VSTTE 2016. LNCS, vol. 9971, pp. 8\u201326. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48869-1_2"},{"key":"21_CR31","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-540-88479-8_22","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"J Sun","year":"2008","unstructured":"Sun, J., Liu, Y., Dong, J.S.: Model checking CSP revisited: introducing a process analysis toolkit. In: Margaria, T., Steffen, B. (eds.) ISoLA 2008. CCIS, vol. 17, pp. 307\u2013322. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88479-8_22"},{"issue":"1\u20132","key":"21_CR32","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1017\/S1471068411000494","volume":"12","author":"J Wielemaker","year":"2012","unstructured":"Wielemaker, J., Schrijvers, T., Triska, M., Lager, T.: Swi-prolog. Theory Pract. Log Program. 12(1\u20132), 67\u201396 (2012). https:\/\/doi.org\/10.1017\/S1471068411000494","journal-title":"Theory Pract. Log Program."},{"key":"21_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-319-46982-9_24","volume-title":"Runtime Verification","author":"Y Yamagata","year":"2016","unstructured":"Yamagata, Y., et al.: Runtime monitoring for concurrent systems. In: Falcone, Y., S\u00e1nchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 386\u2013403. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46982-9_24"}],"container-title":["Lecture Notes in Computer Science","Towards Autonomous Robotic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-01486-3_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,19]],"date-time":"2025-08-19T15:47:03Z","timestamp":1755618423000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-01486-3_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,13]]},"ISBN":["9783032014856","9783032014863"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-01486-3_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,8,13]]},"assertion":[{"value":"13 August 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TAROS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Annual Conference Towards Autonomous Robotic Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"York","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 August 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 August 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"taros2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/taros-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}