Human-Robot Interaction in the Design and Verification of Robotic Systems

Proving properties about robotic systems with humans-in-the-loop relies on assumptions about human behaviour. Existing technologies require expertise not reasonably expected from those with expert knowledge of human behaviour: psychologists and human-factors engineers, for instance. Through a user-needs analysis, of industrial design techniques for human-robot interaction, we identify a lack of standardised approach and devise requirements for a notation for the design and verification of robotic systems with humans in the loop.
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.