|LESTINGI LIVIA||Cycle: XXXV |
Section: Computer Science and Engineering
Tutor: PRADELLA MATTEO
Advisor: ROSSI MATTEO GIOVANNI Major Research topic
:Model-Driven Development of Formally Verified Human-Robot InteractionsAbstract:
The scientific community generally agrees that robots will play a pivotal role in a near-future society. The employment of robotics has already taken a groundbreaking turn, over the last few years, thanks to the introduction of human collaboration in industrial settings. Nevertheless, research is already aiming for the next phase.
Robots will indeed no longer be confined to industrial environments, but they are bound to enter the civil domain as well. Many works endorse the potential of having robots in healthcare or disaster relief situations. Under these premises, robots will be interacting with a huge variety of people with very different needs. Traditionally, a robot's decision-making process has been driven by efficiency-related factors, but this probably will no longer suit users who expect empathy in their everyday interactions. Therefore, in the future robots will be called to include factors related to human physiology and mental and physical state while making decisions.
The hereby presented research addresses these issues while also exploiting the benefits of formal methods. The proposed methodology will adopt a model-driven approach to specify and formally verify scenarios where human-robot interaction is the key element. A possible real-life scenario would feature a personal care robot in a hospital ward that is supposed to escort a newly registered patient to his destination.
The first component of the approach is a continuous-time formal specification of the scenario under analysis. Modeling the environment is considered the biggest challenge when applying formal methods to robotic applications. To tackle the magnitude of human behavior variability, covering only a restricted set of relevant traits may prove to be a viable solution. Going back to the previously described hospital scenario, the patient is likely to be in pain or discomfort, hence involving his/her estimated strain curve in the verification may be instrumental to adjust the mission plan accordingly.
Due to users' lack of familiarity with robots, the methodology must guarantee that some specific properties of the system are always verified. The approach features Statistical Model Checking (SMC) as the selected formal verification techniques to comply with the stochastic nature of the human model. Unlike traditional model-checking, adopting this technique also leads to reasonable verification times, as proven by testing the approach on some early test cases.
The resulting framework will thus feature an innovative take on formal verification of robotic systems while opening the way to their deployment in less controllable environments.