Robots are currently mostly found in industrial settings. In the future, a wider range of environments will benefit from their inclusion. This calls for the development of tools that allow professionals to set up dependable robotic applications in which people productively interact with robots aware of their needs. Given the co-existence of humans and robots, the precise analysis—e.g., through formal verification techniques—of properties related to aspects such as human needs and physiology is of paramount importance. In this paper, we present a formally-based, model-driven approach to design and verify scenarios involving human-robot interactions. Some of the features of our approach are tailored to the healthcare domain, from which our case studies are derived. In our approach, the designer specifies the main parameters of the mission to generate the model of the application, which includes mobile robots, the humans to be served, including some of their physiological features, and the decision-maker that orchestrates the execution. All components are modeled through hybrid automata to capture variables with complex dynamics. The model is verified through Statistical Model Checking (SMC), using the Uppaal tool, to determine the probability of success of the mission. The results are examined by the developer, who iteratively refines the design until the probability of success is satisfactory.

A Model-driven Approach for the Formal Analysis of Human-Robot Interaction Scenarios

L. Lestingi;M. Askarpour;M. M. Bersani;M. G. Rossi
2020-01-01

Abstract

Robots are currently mostly found in industrial settings. In the future, a wider range of environments will benefit from their inclusion. This calls for the development of tools that allow professionals to set up dependable robotic applications in which people productively interact with robots aware of their needs. Given the co-existence of humans and robots, the precise analysis—e.g., through formal verification techniques—of properties related to aspects such as human needs and physiology is of paramount importance. In this paper, we present a formally-based, model-driven approach to design and verify scenarios involving human-robot interactions. Some of the features of our approach are tailored to the healthcare domain, from which our case studies are derived. In our approach, the designer specifies the main parameters of the mission to generate the model of the application, which includes mobile robots, the humans to be served, including some of their physiological features, and the decision-maker that orchestrates the execution. All components are modeled through hybrid automata to capture variables with complex dynamics. The model is verified through Statistical Model Checking (SMC), using the Uppaal tool, to determine the probability of success of the mission. The results are examined by the developer, who iteratively refines the design until the probability of success is satisfactory.
2020
2020 IEEE International Conference on Systems, Man, and Cybernetics (SMC)
service robots , human-robot interaction , model-driven development , statistical model checking
File in questo prodotto:
File Dimensione Formato  
main.pdf

accesso aperto

Descrizione: Accepted Version
: Pre-Print (o Pre-Refereeing)
Dimensione 1.59 MB
Formato Adobe PDF
1.59 MB Adobe PDF Visualizza/Apri
09283204.pdf

Accesso riservato

Descrizione: Publisher's version
: Publisher’s version
Dimensione 1.64 MB
Formato Adobe PDF
1.64 MB Adobe PDF   Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11311/1155630
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 6
social impact