Safety verification for ROS software

Abstract

Os robôs são agora parte do nosso quotidiano e a sua utilidade parece não ter limites. Fabricam os nossos bens, colhem alimentos de plantações e conduzem-nos de um lugar para o outro. A inovação na área da robótica é uma constante, as expectativas são altas, e as responsabilidades que depositamos nos robôs são cada vez maiores; os robôs são a nova definição de sistema crítico. Em parte, este sucesso deve-se à abundância de frameworks livres para o desenvolvimento de sistemas robóticos, como é o caso do Robot Operating System (ROS). A comunidade ROS é numerosa e bastante ativa. O ROS tem sido usado principalmente ao nível da investigação, mas, ultimamente, tem sido a base para vários projetos comerciais ou governamentais. Sendo um ecossistema de componentes de software reutilizáveis, suportado por uma comunidade muito diversa, garantir que sistemas baseados em ROS são confiáveis é da maior importância. No entanto, mostrar que um software robótico é confiável não é, de todo, uma tarefa fácil. Várias técnicas, como a Verificação Formal, Model Checking, Verificação Runtime, entre outras, têm dado inúmeras provas da sua aptidão e eficácia para verificar uma variedade de propriedades críticas, noutros domínios de software. Contudo, se há algo que todos estes métodos têm em comum, é a sua complexidade. É necessária uma formação especializada para uma aplicação eficaz, e a maioria da comunidade ROS não tem tais conhecimentos. Nesta tese, respondemos à questão de como adaptar o estado da arte em técnicas de garantia de qualidade para aplicações ROS, e como torná-las acessíveis a não especialistas. Temos em conta o facto de que a maioria dos sistemas são desenvolvidos em torno do código-fonte, em vez de seguirem práticas de Engenharia à base de modelos. Propomos um fluxo de trabalho unificado que, dado o código-fonte de uma aplicação ROS, extrai modelos automaticamente e, de seguida, aplica uma série de técnicas de verificação, estáticas e dinâmicas, relativamente a propriedades do sistema especificadas pelo utilizador. No caso de as análises detetarem uma violação de propriedades, os resultados podem ser utilizados como guias para a resolução de problemas. Caso contrário, os resultados constituem evidência da confiabilidade do sistema, respetivamente às propriedades, que pode ser usada para construção de um argumento de confiabilidade. Este fluxo de trabalho é implementado na plataforma HAROS, e avaliado com dois estudos de caso em robôs reais. O resultado revelou-se eficaz, quer na construção automática de modelos, quer na deteção de falhas, relativamente a propriedades especificadas pelo utilizador. De um modo geral, esta abordagem foi bem recebida pela comunidade ROS. Vários membros já a usam de forma independente, e estão até a propôr as suas próprias extensões.

Robots are now part of our daily lives and their usefulness is, seemingly, never-ending. They manufacture our goods, harvest our crops and drive us from place to place. Innovation in the field of robotics is constant, expectations are high, and the responsibilities we place on robots are ever increasing; robots are the new definition of safety-critical devices. In part, this success is due to the abundance of open source frameworks to help develop robotic systems, such as the Robot Operating System (ROS). ROS has a large and active community. It was mostly used in research, but is recently finding its way into commercial and government projects as well. With such a diverse community, and being based on an ecosystem of reusable software components, ensuring that ROS-based systems are dependable is paramount. However, showing that robotic software is dependable is not an easy task. Many techniques, such as Formal Verification, Model Checking, Runtime Verification, and more, have proved, over and over, to be capable of verifying a diverse range of properties in other software domains. However, if there is one characteristic that often defines these techniques, it is their steep learning curve. They have a hard requirement on expert knowledge, and the vast majority of the ROS community is composed of non-experts. In this thesis, we answer the research question of how to adapt state-of-the-art quality assurance techniques to ROS applications, and how to make them usable by non-experts. We take into consideration the fact that most systems are developed with a code-first approach, rather than following Model-driven Engineering practices. We propose a unified workflow that takes in ROS application code, automatically extracts system models from it, and then applies a variety of static and dynamic analysis techniques with respect to user-specified properties. If a property violation is detected, the results of the analyses can be used as a debugging aid. Otherwise, they provide compelling evidence to structure a dependability case for the given properties. This workflow is implemented in the HAROS framework, and later evaluated with two robot case studies. We have found this approach to be effective, both at building models and at finding faults for user-specified properties. Overall, it has been well-received in the ROS community. Several members are now independently using it, as well as proposing their own extensions.