{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T15:11:37Z","timestamp":1778080297569,"version":"3.51.4"},"publisher-location":"Singapore","reference-count":37,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819586165","type":"print"},{"value":"9789819586172","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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-981-95-8617-2_5","type":"book-chapter","created":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T14:22:14Z","timestamp":1778077334000},"page":"113-158","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Engineering Safe Robotics Software from\u00a0Simulation Models via\u00a0RoboSim"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4319-4872","authenticated-orcid":false,"given":"Pedro","family":"Ribeiro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9698-5569","authenticated-orcid":false,"given":"Dalay","family":"Almeida","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-5662-6032","authenticated-orcid":false,"given":"Paulo E. R.","family":"Bezerra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0831-1976","authenticated-orcid":false,"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8977-4827","authenticated-orcid":false,"given":"Thierry","family":"Lecomte","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3023-2748","authenticated-orcid":false,"given":"Marcel V. M.","family":"Oliveira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,5,1]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: Modeling in Event-B \u2013 System and Software Engineering. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"5_CR2","doi-asserted-by":"publisher","unstructured":"Afzal, A., Goues, C.L., Hilton, M., Timperley, C.S.: A study on challenges of testing robotic systems. In: 13th IEEE International Conference on Software Testing, Validation and Verification, pp. 96\u2013107 (2020). https:\/\/doi.org\/10.1109\/ICST46399.2020.00020","DOI":"10.1109\/ICST46399.2020.00020"},{"key":"5_CR3","unstructured":"ARP4761: Guidelines and methods for conducting the safety assessment process on civil airborne systems and equipment. Technical Report ARP4761, SAE International, Warrendale, PA, USA (1996). https:\/\/www.sae.org"},{"key":"5_CR4","unstructured":"ASTM: Standard practice for operational risk assessment of small unmanned aircraft systems (sUAS) (2016). https:\/\/www.astm.org"},{"key":"5_CR5","unstructured":"ASTM F3266-20: Standard guide for training for remote pilot in command of unmanned aircraft systems (UAS) endorsement (2020). https:\/\/www.astm.org"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Baxter, J., Cavalcanti, A.L.C., Gazda, M., Hierons, R.M.: Testing using CSP models: time, inputs, and outputs. ACM Trans. Comput. Logic 24(2) (2023). https:\/\/doi.org\/10.1145\/3572837","DOI":"10.1145\/3572837"},{"key":"5_CR7","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s00236-020-00394-3","volume":"59","author":"J Baxter","year":"2022","unstructured":"Baxter, J., Ribeiro, P., Cavalcanti, A.L.C.: Sound reasoning in tock-CSP. Acta Informatica 59, 125\u2013162 (2022). https:\/\/doi.org\/10.1007\/s00236-020-00394-3","journal-title":"Acta Informatica"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Behm, P., Benoit, P., Faivre, A., Meynadier, J.M.: M\u00e9t\u00e9or: a successful application of B in a large project. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM\u201999 \u2013 Formal Methods. Lecture Notes in Computer Science, vol.\u00a01708, pp. 369\u2013387. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48119-2_22","DOI":"10.1007\/3-540-48119-2_22"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Carlson, C.S.: Effective FMEAs: Achieving Safe, Reliable, and Economical Products and Processes using Failure Mode and Effects Analysis. Wiley, Hoboken (2012)","DOI":"10.1002\/9781118312575"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Cavalcanti, A.L.C., et al.: RoboStar technology: a roboticist\u2019s toolbox for combined proof, simulation, and testing. In: Cavalcanti, A.L.C., Dongol, B., Hierons, R., Timmis, J., Woodcock, J.C.P. (eds.) Software Engineering for Robotics. Lecture Notes in Computer Science, pp. 249\u2013293. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-66494-7_9","DOI":"10.1007\/978-3-030-66494-7_9"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Cavalcanti, A.L.C., Baxter, J., Hierons, R.M., Lefticaru, R.: Testing robots using CSP. In: Beyer, D., Keller, C. (eds.) Tests and Proofs, pp. 21\u201338. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-31157-5_2","DOI":"10.1007\/978-3-030-31157-5_2"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Cavalcanti, A.L.C., Miyazawa, A., Schulze, U., Timmis, J.: Bringing RoboStar and RT-Tester together. In: Haxthausen, A.E., Huang, W., Roggenbach, M. (eds.) Applicable Formal Methods for Safe Industrial Products. Lecture Notes in Computer Science, vol. 14165, pp. 16\u201333. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-40132-9_2","DOI":"10.1007\/978-3-031-40132-9_2"},{"key":"5_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.scico.2019.01.004","volume":"174","author":"ALC Cavalcanti","year":"2019","unstructured":"Cavalcanti, A.L.C., et al.: Verified simulation for robotics. Sci. Comput. Program. 174, 1\u201337 (2019). https:\/\/doi.org\/10.1016\/j.scico.2019.01.004","journal-title":"Sci. Comput. Program."},{"key":"5_CR14","unstructured":"CLEARSY: C4B User Manual, v1.2, 19\/09\/2016, CLEARSY (2016)"},{"key":"5_CR15","unstructured":"DO-178C: Software considerations in airborne systems and equipment certification. Technical Report DO-178C, RTCA, Inc., Washington, D.C., USA (2011). https:\/\/www.rtca.org"},{"key":"5_CR16","unstructured":"DO-254: Design assurance guidance for airborne electronic hardware. Technical Report DO-254, RTCA, Inc., Washington, D.C., USA (2000). https:\/\/www.rtca.org"},{"key":"5_CR17","unstructured":"DO-326A: Airworthiness security process specification. Technical Report DO-326A, RTCA, Inc., Washington, D.C., USA (2014). https:\/\/www.rtca.org"},{"key":"5_CR18","unstructured":"EASA: Specific operations risk assessment (SORA) (2019). https:\/\/www.easa.europa.eu"},{"key":"5_CR19","unstructured":"Ericson, C.A.: Hazard Analysis Techniques for System Safety, 2nd edn. Wiley, Hoboken (2015)"},{"key":"5_CR20","unstructured":"FAA: Drones & wildfires \u2013 digital toolkit. https:\/\/www.faa.gov\/sites\/faa.gov\/files\/uas\/resources\/community_engagement\/FAA_drones_wildfires_toolkit.pdf"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 \u2013 a modern refinement checker for CSP. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014). Lecture Notes in Computer Science, vol.\u00a08413, pp. 187\u2013201. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_13","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Guiho, G.D., Hennebert, C.: SACEM software validation (experience report). In: Valette, F., Freeman, P.A., Gaudel, M. (eds.) Proceedings of the 12th International Conference on Software Engineering, Nice, France, 26\u201330 March 1990, pp. 186\u2013191. IEEE Computer Society (1990). https:\/\/doi.org\/10.5555\/100296.100321","DOI":"10.5555\/100296.100321"},{"issue":"5","key":"5_CR23","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1109\/52.57887","volume":"7","author":"A Hall","year":"1990","unstructured":"Hall, A.: Seven myths of formal methods. IEEE Softw. 7(5), 11\u201319 (1990). https:\/\/doi.org\/10.1109\/52.57887","journal-title":"IEEE Softw."},{"key":"5_CR24","unstructured":"International Electrotechnical Commission: Failure modes and effects analysis (FMEA and FMECA). Technical Report IEC 60812:2018, IEC, Geneva, Switzerland (2018)"},{"key":"5_CR25","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102524","volume":"199","author":"T Lecomte","year":"2020","unstructured":"Lecomte, T., D\u00e9harbe, D., Fournier, P., Oliveira, M.: The CLEARSY safety platform: 5 years of research, development and deployment. Sci. Comput. Program. 199, 102524 (2020). https:\/\/doi.org\/10.1016\/j.scico.2020.102524","journal-title":"Sci. Comput. Program."},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Lecomte, T.: Programming the CLEARSY safety platform with B. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) Rigorous State-Based Methods (ABZ 2020). Lecture Notes in Computer Science, vol. 12071, pp. 124\u2013138. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-48077-6_9","DOI":"10.1007\/978-3-030-48077-6_9"},{"key":"5_CR27","doi-asserted-by":"publisher","unstructured":"Lecomte, T., D\u00e9harbe, D., Prun, \u00c9., Mottin, E.: Applying a formal method in industry: a 25-year trajectory. In: da\u00a0Costa\u00a0Cavalheiro, S.A., Fiadeiro, J.L. (eds.) Formal Methods: Foundations and Applications (SBMF 2017). Lecture Notes in Computer Science, vol. 10623, pp. 70\u201387. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70848-5_6","DOI":"10.1007\/978-3-319-70848-5_6"},{"key":"5_CR28","doi-asserted-by":"publisher","unstructured":"Lee, W.S., Grosh, D.L., Tillman, F.A., Lie, C.H.: Fault tree analysis, methods, and applications \u2013 a review. IEEE Trans. Reliab. R-34(3), 194\u2013203 (1985). https:\/\/doi.org\/10.1109\/TR.1985.5222114","DOI":"10.1109\/TR.1985.5222114"},{"key":"5_CR29","doi-asserted-by":"publisher","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003: Formal Methods. Lecture Notes in Computer Science, vol.\u00a02805, pp. 855\u2013874. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45236-2_46","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"5_CR30","doi-asserted-by":"publisher","unstructured":"Leveson, N.G.: Engineering a Safer World: Systems Thinking Applied to Safety. The MIT Press (2012). https:\/\/doi.org\/10.7551\/mitpress\/8179.001.0001","DOI":"10.7551\/mitpress\/8179.001.0001"},{"key":"5_CR31","doi-asserted-by":"publisher","unstructured":"Miyazawa, A., et al.: Diagrammatic physical robot models. Softw. Syst. Model. 1\u201345 (2025). https:\/\/doi.org\/10.1007\/s10270-025-01270-9","DOI":"10.1007\/s10270-025-01270-9"},{"key":"5_CR32","doi-asserted-by":"publisher","unstructured":"Mousavi, M., et al.: Trustworthy autonomous systems through verifiability. IEEE Softw. Mag. 56(2) (2023). https:\/\/doi.org\/10.1109\/MC.2022.3192206","DOI":"10.1109\/MC.2022.3192206"},{"key":"5_CR33","doi-asserted-by":"publisher","unstructured":"Ortega, A., Hochgeschwender, N., Berger, T.: Testing service robots in the field: an experience report. In: IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 165\u2013172. IEEE (2022). https:\/\/doi.org\/10.1109\/IROS47612.2022.9981789","DOI":"10.1109\/IROS47612.2022.9981789"},{"issue":"3","key":"5_CR34","doi-asserted-by":"publisher","first-page":"562","DOI":"10.1111\/risa.12867","volume":"38","author":"A Plioutsias","year":"2018","unstructured":"Plioutsias, A., Karanikas, N., Chatzimihailidou, M.M.: Hazard analysis and safety requirements for small drone operations: to what extent do popular drones embed safety? Risk Anal. 38(3), 562\u2013584 (2018). https:\/\/doi.org\/10.1111\/risa.12867","journal-title":"Risk Anal."},{"key":"5_CR35","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/J.COSREV.2015.03.001","volume":"15","author":"E Ruijters","year":"2015","unstructured":"Ruijters, E., Stoelinga, M.: Fault tree analysis: a survey of the state-of-the-art in modeling, analysis and tools. Comput. Sci. Rev. 15, 29\u201362 (2015). https:\/\/doi.org\/10.1016\/J.COSREV.2015.03.001","journal-title":"Comput. Sci. Rev."},{"key":"5_CR36","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. Series in Computer Science, 2nd edn. Prentice Hall International (1992)"},{"key":"5_CR37","unstructured":"Woodcock, J.C.P., Davies, J.: Using Z - Specification, Refinement, and Proof. Series in Computer Science. Prentice Hall International (1996)"}],"container-title":["Lecture Notes in Computer Science","Engineering Trustworthy Software Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-95-8617-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T14:22:32Z","timestamp":1778077352000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-8617-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9789819586165","9789819586172"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-8617-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"1 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETSS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Summer School on Engineering Trustworthy Software Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Beijing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","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":"17 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setss2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/tis.ios.ac.cn\/SETSS2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}