An Assurance-based Approach to Verification and Validation of Human--Robot Teams

摘要

We present an approach for the verification and validation (V\&V) of robot assistants in the context of human-robot interactions (HRI), to demonstrate their trustworthiness through integral assurances on their safety and functional correctness. Trust in robot assistants will allow them to transition from the laboratory into our everyday lives. The complex and unpredictable nature of the real world in which assistant and service robots operate, the limitations on available V\&V techniques when used individually, and the consequent lack of confidence on the verification results (or assurances), present challenges to overcome. Our approach, called \textit{assurance-based verification}, addresses these challenges by combining formal verification (model checking), simulation-based testing, and user validation in experiments with a real robot. We demonstrate our assurance-based V\&V approach through a handover task, the most critical part of a complex cooperative manufacturing scenario, for which we proposed some safety and liveness requirements to verify and validate. We construct formal models, simulations and an experimental test rig for the HRI. To capture requirements we use temporal logic properties, assertion checkers and informal textual descriptions. This combination of approaches allows V\&V of the HRI task at different levels of modelling detail and thoroughness of exploration, thus overcoming the individual limitations of each method. Should the resulting assurances present discrepancies, an iterative process between the three V\&V techniques takes place until confidence in these assurances is gained from refining and improving the assets (i.e., system and requirement models) to represent the HRI task in a more truthful manner.