Model-driven development of formally verified human-robot interactions


Livia Lestingi, Marcello M. Bersani and Matteo Rossi

Presentation title

Model-driven development of formally verified human-robot interactions

Authors

Livia Lestingi, Marcello M. Bersani and Matteo Rossi

Institution(s)

Polytechnic of Milan

Presentation type

Technical presentation

Abstract

In the future, assistive robots will operate in a broad array of settings, ranging from healthcare to hospitality. The common factor among these sectors is the unpredictability brought by the extensive presence of untrained humans, who will frequently interact with and request services from robots. We present a model-driven framework to design, deploy, and re-configure formally verified human-robot interaction scenarios. The framework applies specifically to scenarios featuring mobile robots operating indoors and providing services to humans which require interaction or synchronization.

The tool-supported framework consists of three macro-phases:

  1. Design-time analysis to configure the formal model (i.e., a Stochastic Hybrid Automata network) of the interactive scenario and estimate the probability of success through model-checking.
  2. Deployment to either directly deploy an executable form of the verified robot controller in the physical setting or simulate it in a virtual environment for further investigation.
  3. Automated model refinement: we have developed an automata learning algorithm that infers a model of human behavior starting from traces collected during deployment or simulations. The goal of this learning procedure is to automatically incorporate human behavior variations or unforeseen occurrences observed at runtime into the formal model.

We have validated all of the framework's phases on use cases from the healthcare setting in the virtual environment, whereas experimentation with a physical robotic device is underway. Adopting this methodology paves the way towards developing robotic applications designed to accommodate human free agency and account for their state of health with the guarantees of formal verification.


Additional material

  • Extended abstract: [pdf]
  • Presentation slides: [pdf]

For more details on this presentation please click the button below: