In the future, assistive robots will spread to everyday settings and regularly interact with humans. This paper introduces a deployment approach for assistive robotic applications where human-robot interaction is the main element. The deployment infrastructure hinges on a model-to-code transformation technique and a ROS-based middleware layer and enables deployment in real life or simulation in a virtual environment. The approach fits into a model-driven framework for the formal verification of interactive scenarios. At design-time, the application analyst estimates the most likely outcome of the robotic mission through Statistical Model Checking of a Stochastic Hybrid Automata network modeling the scenario. We introduce an innovative approach to convert a specific subset of Stochastic Hybrid Automata into executable code to control the robot and respond to human actions. Deploying or simulating the application allows analysts to validate the results obtained at design time or to refine the formal model based on runs in the real or the virtual scene. The methodology’s effectiveness is tested via simulation of use cases from the healthcare setting, which can significantly benefit from this kind of approach thanks to its innovative features related to human physiology and autonomous behavior.


    Zugriff

    Download


    Exportieren, teilen und zitieren



    Titel :

    A Deployment Framework for Formally Verified Human-Robot Interactions



    Erscheinungsdatum :

    2021-01-01



    Medientyp :

    Aufsatz (Zeitschrift)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    Klassifikation :

    DDC:    629



    Efficiency analysis of formally verified adaptive cruise controllers

    Loos, Sarah M. / Witmer, David / Steenkiste, Peter et al. | IEEE | 2013


    Software safety architecture that can be formally verified

    Cossy,M. / STZ Softwaretechnik,DE | Kraftfahrwesen | 2004




    Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified

    S. M. Loos / A. Platzer / L. Nistor | NTIS | 2011