Verification of a search-and-rescue drone with humans in the loop

Abstract

In this presentation we use an example of a search-and-rescue drone, used by mountain rescue teams, to illustrate our approach to develop mathematical models and use them to verify behaviour that depends on human interactions with the drone. The design and development of human-in-the-loop robotic systems, such as the search-and-rescue drone, requires knowledge of the human, software, and hardware components of the system. The verification of these systems require knowledge of those same three components. Through this example we will demonstrate how a Hierarchical Task Analysis can be used to develop conformant sequence diagrams that can capture use cases of interest for verification. We will discuss the notation for our sequence diagrams, which is a variation of UML sequence diagrams tailored to capture time properties and with a view of the system that includes the software, the hardware, and human stakeholders.Our sequence diagram notation integrates within an existing verification framework, namely RoboStar, which provides domain-specific notations to model and verify both control software and robotic platforms. In the presentation, we show the kind of property and verification that we can carry out using our sequence diagrams and RoboStar technology. The presentation will also cover leading tools for modelling and verification of human-in-the-loop robotic systems, namely Circus, Ivy, PVSio-web and how they handle human behaviour within the system design. We will compare our approach with that supported by these tools.Verification is a technique used to prove that the system design and development meets the requirements specified; there are many forms of verification including formal verification, simulation, and testing. Formal verification is a tried and tested method to improve confidence in the correctness of a system, its ability to satisfy design requirements. Due to its application during design time, this confidence can be gained prior to the investing of time and resources into system development. Formal verification outputs mathematical proof artefacts that can be used in safety-case development. This verification technique requires formal models of system behaviour and formal models of the properties to be proved. To perform formal verification on a human-in-the-loop system, the formal model of the system behaviour needs to include a model of the expected human interaction. Whilst the data required for the generation of such a model can be provided by evidence from the fields of Human-Computer Interaction, Psychology, Human-Robot Interaction or Human Factors, this data needs to be gathered in a formal model for verification. On the other hand, requiring professionals with the knowledge of human behaviour to also have the expertise on formal verification is unrealistic. Our sequence diagrams are accessible and readable as a way to capture and communicate expected human behaviour. Moreover, it is possible to generate mathematical models for verification automatically from the sequence diagrams.

Keywords: Drone, Robotics, Modeling, Model, UML, Verification, HRI

DOI: 10.54941/ahfe1003753