Model-Driven Development of Formally Verified Human-Robot Interactions

Service robots will operate in unconstrained environments due to the significant presence of humans. We present a model-driven framework based on formal methods to develop interactive robotic applications designed to handle the uncertainty of human behavior. Users formally model the human-robot interaction scenario, estimate the most likely outcome, and subsequently deploy the application. Collected traces constitute the data pool for an active automata learning algorithm to update the human model based on the accumulated knowledge. We validate the framework on realistic use cases from the healthcare setting.