We present a model-driven approach for the creation of formally verified scenarios involving human-robot interaction in healthcare settings. The work offers an innovative take on the application of formal methods to human modeling, as it incorporates physiology-related aspects. The model, based on the formalism of Hybrid Automata, includes a stochastic component to capture the variability of human behavior, which makes it suitable for Statistical Model Checking. The toolchain is meant to be accessible to a wide range of professional figures. Therefore, we have laid out a user-friendly representation format for the scenario, from which the full formal model is automatically generated and verified through the Uppaal tool. The outcome is an estimation of the probability of success of the mission, based on which the user can refine the model if the result is not satisfactory.

Formal Verification of Human-Robot Interaction in Healthcare Scenarios

Lestingi, Livia;Askarpour, Mehrnoosh;Bersani, Marcello M.;Rossi, Matteo
2020-01-01

Abstract

We present a model-driven approach for the creation of formally verified scenarios involving human-robot interaction in healthcare settings. The work offers an innovative take on the application of formal methods to human modeling, as it incorporates physiology-related aspects. The model, based on the formalism of Hybrid Automata, includes a stochastic component to capture the variability of human behavior, which makes it suitable for Statistical Model Checking. The toolchain is meant to be accessible to a wide range of professional figures. Therefore, we have laid out a user-friendly representation format for the scenario, from which the full formal model is automatically generated and verified through the Uppaal tool. The outcome is an estimation of the probability of success of the mission, based on which the user can refine the model if the result is not satisfactory.
Software Engineering and Formal Methods
978-3-030-58767-3
978-3-030-58768-0
File in questo prodotto:
File Dimensione Formato  
SEFM20.pdf

Accesso riservato

Descrizione: Publisher's Version
: Publisher’s version
Dimensione 2.19 MB
Formato Adobe PDF
2.19 MB Adobe PDF   Visualizza/Apri
main.pdf

accesso aperto

Descrizione: Accepted Version
: Post-Print (DRAFT o Author’s Accepted Manuscript-AAM)
Dimensione 1.9 MB
Formato Adobe PDF
1.9 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/1146286
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 5
social impact