Specification, stochastic modeling and analysis of interactive service robotic applications

Assistive robotic systems are quickly becoming a core technology for the service sector as they are understood capable of supporting people in need of assistance in a wide variety of tasks. This step poses a number of ethical and technological questions. The research community is wondering how service robotics can be a step forward in human care and aid, and how robotics applications can be realized in order to put the human role at the forefront. Therefore, there is a growing demand for frameworks supporting robotic application designers in a “human-aware” development process. This paper presents a model-driven framework for analyzing and developing human–robot interactive scenarios in non-industrial settings with significant sources of uncertainty. The framework’s core is a formal model of the agents at play – the humans and the robot – and the robot’s mission, which is then put through verification to estimate the probability of completing the mission. The model captures non-trivial features related to human behavior, specifically the unpredictability of human choices and physiological aspects tied to their state of health. To foster the framework’s accessibility, we present a verification tool-agnostic Domain-Specific Language that allows designers lacking expertise in formal modeling to configure the interactive scenarios in a user-friendly manner. We compare the formal analysis outputs with results obtained by deploying benchmark scenarios in the physical environment with a real mobile robot to assess whether the formal model adheres to reality and whether the verification results are accurate. The entire development pipeline is then tested on several scenarios from the healthcare setting to assess its flexibility and effectiveness in the application design process.