|LESTINGI LIVIA||Cycle: XXXV |
Section: Computer Science and Engineering
Tutor: PRADELLA MATTEO
Advisor: ROSSI MATTEO GIOVANNI Major Research topic
:Formally Verified Human-Robot InteractionAbstract:
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. State-of-the-art applications can simultaneously rely on robots' capability to withstand dull and fatiguing tasks and on human creative skills. 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. For example, many works endorse the potential of having robots in healthcare or disaster relief situations. Such a technology shift would decrease the operational distance between humans and robots even further. Firstly, this calls for a renewed outlook on safety measures during operation. Since users will not necessarily possess a technical background, currently available robot programming tools also constitute an entry barrier. The hereby presented research activity aims at paving the way to solve these issues.
The proposed methodology will adopt a model-driven approach to specify robotic missions. The person in charge of designing the task will have the possibility to start from programming primitives previously defined by developers and arrange them into more complex patterns. The resulting constructs will be templates of non-elementary tasks whose detailed plan will depend on parameters provided by the user at deployment time. For instance, a possible real-life scenario would feature a healthcare assistant robot in a hospital setting that is supposed to escort a newly registered patient to his destination. In this case, the ER registration clerk would only have to select the proper set of inputs (e.g., the destination) to run the task. This will relieve users of the cumbersome task of implementing low-level routines, e.g., robot movement, which requires prior expertise in the robotic field.
Due to users' lack of familiarity with robots, the methodology must be highly reliable. A continuous-time formal specification underlying the modeling layer makes it possible to guarantee that specific properties of the system are always verified. Given the diversity of scenarios under consideration, these properties will be equally diverse. The fundamental assumption is that modeled tasks will include one -or more- robots interacting with the environment. The verification process thus ought to take into account the robot inner features. If the robot is mobile, analyzing the battery discharging cycle is essential to know when it will have to reach the charging dock and how this will affect the overall workflow. Modeling the environment is universally considered the biggest challenge when designing a Domain-Specific-Language for robotics. 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. The resulting framework would thus feature an innovative take on formal verification of robotic systems while opening the way to their deployment in less controllable environments.