HRC-Team : a model-driven approach to formal verification and deployment of collaborative robotic applications

Collaborative robotic applications are becoming increasingly widespread as a result of the Industry 4.0 phenomenon. This innovation, albeit instrumental in improving production lines flexibility, raises 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. This Thesis introduces a tool-supported model-driven approach facing these issues. The proposal provides an intuitive graphical notation from which formal logic models, at the heart of the SAFER-HRC methodology, are automatically generated. The results of the formal verification process provide insight into the task’s overall safety conditions, on the basis of which the user can modify the model in order to bring the estimated risk level below a certain threshold. The tool is also able to translate the model into a hybrid IEC 61499 - ROS architecture. The generated Function Block application can either be deployed on physical or emulated resources. In order to achieve this result, the user is required to create a set of UML diagrams, constituting the custom HRC-TEAM Profile, through the Papyrus modeling tool. This comprises Class Diagrams for the definition of available resources and Component Diagrams for a detailed description of their inner architectures. Once the operational environment is laid out, Activity Diagrams are used to define the application’s workflow. Standard UML semantics, often overly generic to meet domain-specific demands, has been extended through stereotypes which need to be dynamically applied to the produced models. The illustrated toolchain supports users throughout the whole application design, testing and execution process, enabling successive refinements thanks to its automated nature. Moreover, its visual notation and high automation degree make it accessible to a wider public with varying levels of expertise. Finally, the approach has been tested against realistic case studies in order to evaluate its efficiency and assess its usability.

Grazie al fenomeno conosciuto come Industria 4.0, la robotica collaborativa sta subendo una notevole diffusione come tecnologia fulcro delle applicazioni industriali. Tale evoluzione, per quanto fondamentale nell'incrementare la flessibilità delle linee di produzione, solleva questioni relative alla sicurezza a causa dello stretto contatto tra umani e robot. Tuttavia, le attuali tecniche per la valutazione del rischio richiedono tempi di realizzazione tendenzialmente lunghi e una preparazione di carattere scientifico che spesso manca agli operatori. Questa Tesi introduce un approccio basato su modelli astratti e supportato da un tool automatico, il quale, a partire da una notazione grafica intuitiva, genera modelli di logica formale alla base della metodologia SAFER-HRC. I risultati del processo di verifica formale forniscono un quadro delle condizioni di sicurezza della task, in base al quale l’utente può modificare il modello fino a riportare il livello di rischio sotto la soglia desiderata. Lo strumento permette anche la traduzione del modello in un’architettura ibrida basata sullo standard IEC61499 e ROS. L’applicazione di Function Block così generata può essere, quindi, eseguita su risorse fisiche o simulate in ambiente virtuale. Per ottenere questi risultati, all'utente è richiesta la creazione di diagrammi UML, costituenti il profilo HRC-TEAM, tramite il software di modellazione Papyrus. Questo include Class Diagram per la definizione delle risorse disponibili e Component Diagram per una rappresenzazione dettagliata delle relative strutture interne. Una volta definito il contesto operativo, gli Activity Diagram sono impiegati per definire il workflow dell’applicazione. Al fine di soddisfare le esigenze di modellazione dovute al contesto specifico, la semantica dell'UML, ove eccessivamente generica, è stata estesa tramite stereotipi da applicare dinamicamente ai modelli in fase di elaborazione. La procedura illustrata assiste l’utente durante l’intero processo di progettazione, testing ed esecuzione dell’applicazione, consentendo un progressivo raffinamento del modello. Inoltre, la natura visiva della notazione e l’alto livello di automazione la rendono accessibile a un bacino di utenti più vasto e con diverso grado di esperienza. Infine, l’approccio è stato testato su casi di studio realistici per valutarne in modo più concreto efficacia e facilità d’uso.