Model-driven development of formally verified human-robot interactions

In a near-future society, robots will no longer be confined to industrial environments but are bound to enter the service sector, where they will interact with a wide variety of people with very different needs. Efficiency-related factors drive existing software development techniques, but this will no longer suit everyday interactions. Incorporating factors related to the human behavioral and physiological state into the development process will become essential. This research addresses these issues by proposing a model-driven approach to design, formally verify, and adjust scenarios where human-robot interaction is a primary element. Target users of the approach are professionals in charge of designing the robotic application but lacking solid technical background, which motivates the high degree of automation of the whole development toolchain. The entry point to the approach is a user-friendly Domain-Specific Language to specify the scenario and the robotic mission under analysis. A formal model of the scenario based on Stochastic Hybrid Automata is then automatically generated. The approach captures a set of physiological traits---including physical fatigue---and behavioral traits capturing the possibility of the human making haphazard decisions. The formal model is subject to Statistical Model Checking to estimate the most likely mission's outcome. Subsequently, the approach features a deployment framework to deploy the scenario in a real setting or simulate it in a virtual environment for further investigation. The configured model of the interactive scenario is transformed into an executable version to ensure that properties formally verified at design time also hold at runtime. Data collected during deployment are exploited to infer an updated model of human behavior and adjust the robotic mission accordingly. To this end, we introduce an automata learning algorithm called L*_SHA specifically targeting Stochastic Hybrid Automata. The learned model of human behavior is plugged into the Stochastic Hybrid Automata network to perform a new round of verification and revise the mission's design, if necessary. All phases of the model-driven approach---the design-time analysis, deployment, and automata learning---have been empirically validated on realistic case studies inspired by healthcare scenarios. The formal foundation is a key component in guaranteeing the dependability of the resulting software components. At the same time, the high-level abstraction level and the presence of a learning procedure promote the framework's flexibility.

In un futuro prossimo, i robot non saranno più confinati all'ambito industriale ma verranno largamente impiegati nel settore dei servizi, dove interagiranno con un'ampia varietà di persone con diverse esigenze. Fattori legati all'efficienza sono alla base di tecniche di ingegneria del software già esistenti, ma ciò non sarà più sufficiente per le interazioni tra uomo e robot nella vita di tutti i giorni. Diventerà, infatti, essenziale incorporare fattori legati allo stato comportamentale e fisiologico umano nel processo di sviluppo del software. Questo progetto di ricerca affronta quest'esigenza emergente proponendo un framework model-driven per progettare, verificare formalmente e ri-configurare scenari in cui l'interazione uomo-robot è un elemento primario. Gli utenti a cui è destinato l'approccio sono figure professionali responsabili per la progettazione dell'applicazione robotica ma privi di un solido background tecnico, il che motiva l'elevato grado di automazione del processo di sviluppo. Il punto di ingresso al framework è un domain-specific language accessibile per specificare le caratteristiche dello scenario e la missione robotica soggetti ad analisi. Successivamente, viene generato automaticamente un modello formale dello scenario basato su Stochastic Hybrid Automata. L'approccio include una serie di tratti fisiologici dei soggetti umani, inclusa la fatica fisica, e tratti comportamentali, quali la possibilità che l'essere umano prenda decisioni inaspettate. Il modello formale è soggetto a Statistical Model Checking per stimare l'esito più probabile della missione robotica. In una fase successiva, il framework prevede un approccio per il deployment dello scenario in un ambiente reale o la simulazione in un ambiente virtuale per ulteriori indagini. Il modello formale dello scenario interattivo viene trasformato in una versione eseguibile per garantire che le proprietà verificate formalmente in fase di progettazione valgano anche in fase di esecuzione. I dati raccolti sul campo durante l'esecuzione della missione vengono sfruttati per apprendere un modello aggiornato del comportamento umano e adattare di conseguenza la missione robotica. A tal fine, introduciamo un algoritmo di automata learning chiamato L*_SHA specifico per Stochastic Hybrid Automata. Il modello appreso del comportamento umano viene inserito nella rete di Stochastic Hybrid Automata per eseguire un nuovo ciclo di verifica e modificare la missione, se necessario. Tutte le fasi del framework---l'analisi in fase di progettazione, l'implementazione e l'apprendimento degli automi---sono state convalidate empiricamente su casi di studio realistici ispirati a scenari dall'ambito medico-sanitario. La base formale è una componente chiave per garantire l'affidabilità dei componenti software risultanti. Allo stesso tempo, l'alto livello di astrazione e la presenza di una procedura di apprendimento favoriscono la flessibilità del framework.