Safer-HRC: a methodology for safety assessment through formal verification in human-robot collaboration

Robots usually function in workspaces divided (e.g., by fences) from those of human operators. However, novel robotic and cyber-physical systems have evolved in size and functionality to include the collaboration with human operators within common workspaces. This new application field is often referred to as Human-Robot Collaboration (HRC) and is increasingly prominent in people’s lives and in industrial domains, for example in manufacturing applications. However, HRC raises new challenges to guarantee system safety, due to the presence of operators. Close proximity and frequent physical contacts between operators and robots, and intrinsic non-determinism in operators’ behavior make it difficult for safety assessors and analyzers to cope with the dynamism of collaborative applications. Yet, formal verification techniques can help in this regard through the exhaustive state-space exploration of system models, which can identify unwanted situations early in the development process. In fact, this thesis proposes to use formal verification techniques for analyzing risks in HRC, through a methodology which is compatible with well-known standards in the area of collaborative robotics. In particular, the methodology relies on temporal logicbased models to describe the different possible ways in which tasks can be carried out, and on fully automated formal verification techniques to explore the corresponding state-space to detect and modify the hazardous situations at early stages of system design. This innovative methodology, called SAFER-HRC, is centered around TRIO temporal logic language and Zot bounded satisfiability checker, to assess the safety risks in an HRC application. This work focuses on mechanical hazards which unlike other types (e.g., thermal, electrical,etc.), are results of human-robot interaction. The methodology starts from a generic modular formal model and customizes it for the target system; It then iteratively checks the model against certain safety properties, to study the safety of the collaborative environment for human operators. The generic model contains a non-deterministic formal model of operator behavior which captures the hazardous situations resulting from human errors. This method has an iterative and incremental nature, and allows safety engineers to refine their designs until all plausible erroneous behaviors are considered and mitigated. Finally, this thesis introduces a tool-supported approach for the automated generation of formal models from a semi-formal language, in particular UML. The tool prototype is based on Papyrus UML modeler that provides mechanisms to allow safety engineers, who are typically not experts in formal methods, to automatically generate and formally verify logical models from a UML-based notation which is more attuned with their background.

Nelle applicazioni di robotica classiche, c’è sempre una separazione concreta tra il robot e operatori umani. Solitamente robot operano in spazi di lavoro divisi da quelli degli operatori umani (p.es. via recinzioni). Recentemente i nuovi sistemi robotici e cyber-fisici si sono evoluti in termini di dimensioni e funzionalità, al fine di includere la collaborazione con gli operatori umani all’interno di spazi comuni di lavoro. Questo nuovo contesto è spesso definito come Human-Robot Collaboration (HRC) e sta diventando sempre piu importante nella vita quotidiana delle persone e nei settori industriali, ad esempio nelle applicazioni manifatturiere. Tuttavia, la HRC favorisce nuove sfide al fine di garantire la sicurezza del sistema a causa della presenza di operatori. La vicinanza e frequenti contatti fisici tra i operatori e i robot, e inoltre il non-determinismo del comportamento degli operatori rendono difficile per gli analizzatori di sicurezza affrontare il dinamismo delle applicazioni collaborative. Nonostante ciò, le tecniche di verifica formale possono affrontare questa problematicità attraverso una esauriente esplorazione di modelli di sistemi che consentono di individuare situazioni indesiderate all’inizio del processo di sviluppo. La presente tesi propone di utilizzare tecniche formali di verifica per analizzare i rischi nel’applicazioni HRC, tramite una metodologia compatibile con gli standard conosciuti nell’ambito della robotica collaborativa. In particolare, la metodologia si affida su (i) modelli temporali logici per descrivere i diversi modi possibili in cui i lavori possono essere eseguiti, (ii) e su tecniche di verifica formale completamente automatizzate per esplorare lo state-space corrispondente per rilevare e modificare le situazioni pericolose nelle fasi iniziali di progettazione del sistema. Questa metodologia innovativa che si chiama SAFER-HRC, utilizza il linguaggio logico temporale TRIO e Zot, un bounded satisfiability checker, per valutare i rischi di sicurezza in un’applicazione HRC. Il lavoro si concentra sui rischi meccanici che, al contrario di altri (p.es. termici, elettrici, ecc.), derivano dall’interazione di uomo-robot. Tale metodologia prende le mosse da un modello modulare generico e lo adatta al sistema analizzato in modo da verificare iterativamente determinate proprietà, al fine di studiare la sicurezza degli operatori umani nell’ambiente collaborativo. Il modello generico contiene un ricco formalismo non-deterministico del comportamento dell’operatore che cattura le situazioni pericolose derivanti da errori umani. Questo metodo è iterativo e incrementale e consente agli esperti di sicurezza di perfezionare la progettazione del sistema finchè non vengono considerati e mitigati tutti i comportamenti erronei plausibili. Infine, questa tesi presenta un approccio metodologico ed un prototipo per la generazione automatica di modelli formali a partire da un linguaggio semi-formale. Lo strumento risultante, implementato come plugin del noto software di modellizzazione UML Papyrus, consente agli esperti di sicurezza, che non sono tipicamente conoscitori di metodi formali, di generare automaticamente e verificare formalmente i modelli logici da una notazione basata su UML, più attinente alle loro conoscenze.