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. This prospect calls for solutions to handle uncertainties from a software engineering perspective, starting from an early design stage of the interactive robotic application. This work targets this issue by proposing 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 approach is general-purpose, although selected use cases relate to the healthcare setting.

Related Publications:

• 10.1007/s10270-023-01125-1
• 10.1016/j.robot.2023.104387
• 10.1109/MIS.2022.3215698
• 10.1109/ACCESS.2021.3117852
• 10.1145/3524482.3527653
• 10.1109/SMC42975.2020.9283204
• 10.1007/978-3-030-58768-0_17
• arXiv:2007.11738

A crucial challenge for future software-intensive intelligent systems is their capability to explain specific results and decisions in a human-interpretable manner. Within this line of work, the work focuses on designing innovative software architectures for systems with different levels of explainability capabilities, exploiting interactive service robotic applications as an illustrative use case.

Related Publications:

• 10.1109/REW57809.2023.00059
• 10.1007/978-3-031-42592-9_11
• 10.1109/FormaliSE58978.2023.00010
• 10.1109/ICSA-C57050.2023.00029

Empathy is the human ability to relate to one another's inner state, and emotions are crucial to achieving empathy. The theory of affective computing suggests that we should make computers perceive and display emotions to appear "genuinely intelligent" and interact with humans naturally. This research project aims at developing a formal model of the participants in the conversation---the human user and the agent---to verify whether the agent successfully guides the user towards the target emotional state.

Automata learning techniques can become a pivotal phase for software development toolchains targeting CPSs whose behavior is only partially known or partially observable. Within this line of research, a novel active automata learning algorithm has been developed, which infers Stochastic Hybrid Automata from sensor-collected field data. Learned models can be exploited to analyze or predict CPS behavior. Also, models can be embedded into novel controller synthesis techniques that optimize relevant quality metrics in light of the newly discovered knowledge about the CPS.

Related Publications:

• 10.1109/MIS.2022.3215698

Collaborative robotic applications are becoming increasingly widespread, raising safety issues due to humans and robots working in close proximity. Current risk assessment methods, though, are either overly time-consuming or require a strong scientific background which practitioners usually lack. We introduce a UML-based intuitive graphical notation from which formal logic models conforming to the SAFER-HRC methodology are automatically generated. The results of the formal verification process provide insight into the task's overall safety conditions. Finally, the tool translates the model into a deployable hybrid IEC 61499 - ROS architecture.

Related Publications:

• 10.1007/s10846-021-01386-2
• 10.1109/ICHMS49158.2020.9209450