{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T04:11:24Z","timestamp":1746072684099,"version":"3.40.4"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031908996","type":"print"},{"value":"9783031909009","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Proving properties about robotic systems with humans-in-the-loop relies on assumptions about human behaviour. Existing technologies require expertise not reasonably expected from psychologists and human-factors engineers, for instance. A user-needs analysis of industrial design techniques for human-robot interaction has identified a lack of standardised approach. We present RoboScene, a notation based on UML sequence diagrams that can be used to capture assumptions derived from human-factors artefacts, through novel constructs enabling consideration of stakeholders with different traits. We describe a tock-CSP semantics for RoboScene, and show how we can connect (mathematically) RoboScene diagrams to platform-independent software models. This is applied in the context of a Human-Centered Engineering process, demonstrated via an industrial case study.<\/jats:p>","DOI":"10.1007\/978-3-031-90900-9_9","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:43:45Z","timestamp":1745988225000},"page":"166-187","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["RoboScene: Notation for Formal Verification of Human-Robot Interaction"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7241-5905","authenticated-orcid":false,"given":"Holly","family":"Hendry","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0831-1976","authenticated-orcid":false,"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0746-8899","authenticated-orcid":false,"given":"Cade","family":"McCall","sequence":"additional","affiliation":[]},{"given":"Mark","family":"Chattington","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","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","DOI":"10.1007\/s00236-020-00394-3"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Bolton, M., Bass, E.: A Method for the Formal Verification of Human-interactive Systems. Proc. of the HFES Annual Meeting 52, 764\u2013768 (11 2009)","DOI":"10.1518\/107118109X12524442637309"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Braun, V., Clarke, V.: Using thematic analysis in psychology. Qualitative Research in Psychology 3, 77\u2013101 (01 2006)","DOI":"10.1191\/1478088706qp063oa"},{"key":"9_CR4","unstructured":"Campos, J.: IVY Workbench, http:\/\/ivy.di.uminho.pt\/"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Cavalcanti, A., Baxter, J., Hierons, R., Lefticaru, R.: Testing robots using CSP (September 2019), https:\/\/eprints.whiterose.ac.uk\/150135\/","DOI":"10.1007\/978-3-030-31157-5_2"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Cavalcanti, A.: Modelling and Verification of Robotic Platforms for Simulation Using RoboStar Technology, pp.\u00a03\u20135. Springer International Publishing (05 2020)","DOI":"10.1007\/978-3-030-48077-6_1"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Cavalcanti, A., Barnett, W., Baxter, J., Carvalho, G., Filho, M.C., Miyazawa, A., Ribeiro, P., Sampaio, A.: RoboStar Technology: A Roboticist\u2019s Toolbox for Combined Proof, Simulation, and Testing. Software Engineering for Robotics (2020)","DOI":"10.1007\/978-3-030-66494-7_9"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Chen, X., Mallet, F., Liu, X.: Formally Verifying Sequence Diagrams for Safety Critical Systems. In: TASE 2020. pp. 217\u2013224 (2020)","DOI":"10.1109\/TASE49443.2020.00037"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Chen, Z., Zhenhua, D.: Specification and Verification of UML2.0 Sequence Diagrams Using Event Deterministic Finite Automata. In: SSIRI-C 2011. pp. 41\u201346 (2011)","DOI":"10.1109\/SSIRI-C.2011.17"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Choi, B., Park, J., Park, C.H.: Formal Verification for Human-Robot Interaction in Medical Environments. In: HRI \u201921 Companion. pp. 181\u2013185 (03 2021)","DOI":"10.1145\/3434074.3447155"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Cunha, E., Custodio, M., Rocha, H., Barreto, R.: Formal Verification of UML Sequence Diagrams in the Embedded Systems Context. In: SBESC 2011. pp. 39\u201345 (2011)","DOI":"10.1109\/SBESC.2011.18"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Donkin, C., Little, D.R., Houpt, J.W.: Assessing the speed\u2013accuracy trade-off effect on the capacity of information processing. J Exp Psychol Hum Percept Perform 40(3), 1183\u20131202 (Mar 2014)","DOI":"10.1037\/a0035947"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Ejnioui, A., Otero, C.E., Qureshi, A.A.: Formal semantics of interactions in sequence diagrams for embedded software. In: 2013 ICOS. pp. 106\u2013111 (2013)","DOI":"10.1109\/ICOS.2013.6735057"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 - A Modern Refinement Checker for CSP. In: Tools and Algorithms for the Construction and Analysis of Systems. pp. 187\u2013201 (2014)","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Hart, S., Steane, V., Bullock, S., Noyes, J.M.: Understanding human decision-making when controlling UAVs in a search and rescue application. In: IHIET 2022: Artificial Intelligence & Future Applications. AHFE International (2022)","DOI":"10.54941\/ahfe1002768"},{"key":"9_CR16","unstructured":"Hendry, H., Cavalcanti, A., McCall, C., Chattington, M.: Modelling of Human Behaviour in Robotic Systems, https:\/\/robostar.cs.york.ac.uk\/publications\/reports\/Human_Behaviour_in_RS.pdf, Working Paper\/Draft"},{"key":"9_CR17","unstructured":"Hendry, H., Cavalcanti, A., McCall, C., Chattington, M.: RoboScene Materials, https:\/\/github.com\/UoY-RoboStar\/RoboScene"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Hoare, C.: Communicating Sequential Process. CACM 21, 666\u2013677 (08 1978)","DOI":"10.1145\/359576.359585"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Jacobs, J., Simpson, A.: On a Process Algebraic Representation of Sequence Diagrams. In: Canal, C., Idani, A. (eds.) Software Engineering and Formal Methods. pp. 71\u201385. Springer International Publishing (2015)","DOI":"10.1007\/978-3-319-15201-1_5"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Kaizu, T., Isobe, Y., Suzuki, M.: Refinement and Verification of Sequence Diagrams Using the Process Algebra CSP. IEICE Trans. Fundam. Electron. Commun. Comput. Sci. 96-A, 495\u2013504 (2013)","DOI":"10.1587\/transfun.E96.A.495"},{"key":"9_CR21","unstructured":"Kutar, M., Britton, C., Barker, T.: A Comparison of Empirical Study and Cognitive Dimensions Analysis in the Evaluation of UML Diagrams. In: Proc. of the 14th Workshop of the PPIG (01 2002)"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Li, X., Liu, Z., Jifeng, H.: A formal semantics of UML sequence diagram. In: 2004 ASWEC Proc. pp. 168\u2013177 (2004)","DOI":"10.1109\/ASWEC.2004.1290469"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Lima, V., Talhi, C., Mouheb, D., Debbabi, M., Wang, L., Pourzandi, M.: Formal Verification and Validation of UML 2.0 Sequence Diagrams using Source and Destination of Messages. Electr. Notes Theor. Comput. Sci. 254, 143\u2013160 (10 2009)","DOI":"10.1016\/j.entcs.2009.09.064"},{"key":"9_CR24","unstructured":"Martinie, C., Navarre, D., Palanque, P., Barboni, E., Pottier, G., Winckler, M.: Circus Tool Suite, https:\/\/www.irit.fr\/recherches\/ICS\/softwares\/circus\/"},{"key":"9_CR25","unstructured":"Masci, P., Oladimeji, P.: PVSio-web, http:\/\/www.pvsioweb.org"},{"key":"9_CR26","unstructured":"Microsoft Corporation: Microsoft visio (2024), https:\/\/products.office.com\/en\/visio\/flowchart-software"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Miyazawa, A., Ribeiro, P., Li, W., Cavalcanti, A., Timmis, J., Woodcock, J.: RoboChart: modelling and verification of the functional behaviour of robotic applications. Software & Systems Modeling 18, 1\u201353 (10 2019)","DOI":"10.1007\/s10270-018-00710-z"},{"key":"9_CR28","doi-asserted-by":"publisher","unstructured":"Muram, F.U., Tran, H., Zdun, U.: A model checking based approach for containment checking of uml sequence diagrams. In: 2016 23rd Asia-Pacific Software Engineering Conference (APSEC). pp. 73\u201380 (2016). https:\/\/doi.org\/10.1109\/APSEC.2016.021","DOI":"10.1109\/APSEC.2016.021"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"do\u00a0Nascimento, F.A.M., da\u00a0Silva\u00a0Oliveira, M.F., Wagner, F.R.: Using MDE for the Formal Verification of Embedded Systems Modeled by UML Sequence Diagrams. In: SBCCI\u201909. SBCCI \u201909, ACM, New York, NY, USA (2009)","DOI":"10.1145\/1601896.1601962"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) Automated Deduction\u2014CADE-11. vol.\u00a0607, pp. 748\u2013752. Springer, Berlin, Heidelberg (02 2001)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Rom\u00e1n, C.A.F., DeLuca, J., Yao, B., Genova, H.M., Wylie, G.R.: Signal Detection Theory as a Novel Tool to Understand Cognitive Fatigue in Individuals With Multiple Sclerosis. Front Behav Neurosci 16, 828566 (Mar 2022)","DOI":"10.3389\/fnbeh.2022.828566"},{"key":"9_CR32","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall Series in Computer Science, Prentice-Hall (1998)"},{"key":"9_CR33","unstructured":"Sadigh, D., Driggs-Campbell, K., Puggelli, A., Li, W., Shia, V., Bajcsy, R., Vincentelli, A., Sastry, S., Seshia, S.: Data-Driven Probabilistic Modeling and Verification of Human Driver Behavior. In: AAAI Spring Symposium. pp. 55\u201361 (03 2014)"},{"key":"9_CR34","unstructured":"Sadigh, D., Sastry, S., Seshia, S., Dragan, A.: Planning for Autonomous Cars that Leverage Effects on Human Actions. In: Robotics: Science and Systems (06 2016)"},{"key":"9_CR35","doi-asserted-by":"crossref","unstructured":"Saputra, A.B., Basuki, T.A., Tirtawangsa, J.: Transformation of UML 2.0 sequence diagram into Coloured Petri Nets. In: 2014 ICAICTA. pp. 243\u2013248 (2014)","DOI":"10.1109\/ICAICTA.2014.7005948"},{"key":"9_CR36","unstructured":"Shen, H., Robinson, M., Niu, J.: A Logical Framework for Sequence Diagram with Combined Fragments (2011), https:\/\/api.semanticscholar.org\/CorpusID:8677948"},{"key":"9_CR37","doi-asserted-by":"crossref","unstructured":"Shepherd, A.: HTA as a framework for task analysis. Ergonomics 41, 1537\u201352 (12 1998)","DOI":"10.1080\/001401398186063"},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"Windsor, M., Cavalcanti, A.: RoboCert: Property Specification in Robotics. In: Riesco, A., Zhang, M. (eds.) Formal Methods and Software Engineering. pp. 386\u2013403. Springer (2022)","DOI":"10.1007\/978-3-031-17244-1_23"},{"key":"9_CR39","doi-asserted-by":"crossref","unstructured":"Zafar, N.: Formal Specification and Verification of Few Combined Fragments of UML Sequence Diagram. Arabian Journal for Science and Engineering 41 (02 2016)","DOI":"10.1007\/s13369-015-1999-9"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90900-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:44:16Z","timestamp":1745988256000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90900-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031908996","9783031909009"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90900-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/fase\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}