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.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.