Analysis of message passing software using electrum

Abstract

Automation developments are enabling industrial restructuring through the incorporation of more efficient and accurate processes with less associated cost. Consequently, robots are being increasingly used in the most various scenarios, including in Safety Critical domains. In such cases, the use of suitable methods to attest both the system’s quality and their safety is absolutely essential. Following the current increase of complexity of cyber-physical systems, safety guards which used to be fully hardware dependent, are constantly migrating to software. Here upon, middleware software to abstract systems hardware are constantly evolving and are being increasingly adopted. The common feature of these systems is usually associated with its modular architectures based on message-passing communication patterns. A notorious case is the ROS middleware, where highly configurable robots are usually built by composing third-party modules. The verification of such systems is usually very hard, and its implemen tation in real industrial environments is, in most cases, impracticable. To promote adoption, this work advocates the use of lightweight formal methods associated with semi-automatic techniques that require minimal user input and provide valuable intuitive feedback. This work explores and proposes a technique to automatically verify system-wide safety properties of ROS-based applications in continuous integration environments. It is based on the formalization of ROS architectural models and nodes behaviours in Electrum, a specification language of first-order temporal logic supported by a model-finder over which, system-wide properties are subsequently model-checked. In order to automate the analysis, the technique is deployed as an HAROS plug-in, a framework for quality assessment of ROS software, specially aimed to its community. The technique proposal and its implementation under the HAROS framework are eval uated with positive results on a real agricultural robot, AgRobV16, whose dimension and complexity are industrially representative.

O constante desenvolvimento em processos de automação tem motivado reestruturações nos mais diversos processos industriais, aumentando a sua eficiência, e consequentemente, reduzindo os custos associados. As vantagens provocadas pela automação impulsionam a sua adoção nos mais amplos domínios, nomeadamente, em cenários considerados críticos. Nestes casos, é vital a existência e adopção de técnicas que forneçam fortes garantias da qualidade e segurança dos sistemas. Isto é de particular relevância aquando do desenvolvimento de sistemas ciber-físicos, onde se observa uma constante migração de safety guards, que eram usualmente implementadas ao nível do hardware, para lógica de software. De forma a acompanhar o aumento na complexidade destes sistemas, middlewares que permitem abstrair hardware tem sido adoptados de forma ubíqua. Este são construídos predominantemente sobre arquiteturas modulares baseadas em message-passing. Um caso notório são as aplicações ROS, onde robôs altamente configuráveis são construídos através da composição de módulos externos. Na maioria dos casos, a verificação destes sistemas é muito difícil, sendo que em ambientes industriais e geralmente impraticável. Com vista a promover a adopção de técnicas que promovam a qualidade do software em ambientes de produção, este trabalho defende a utilização de lightweight formal methods associados a técnicas semi-automáticas que requerem intervenções mínimas por parte dos utilizadores, retornando feedback valioso de forma intuitiva. Este trabalho explora e propõe uma técnica para verificação automática de system-wide safety properties em aplicações ROS, cujos resultados podem ser estendidos para qualquer arquitetura modular baseada em message passing. A técnica fundamenta-se na formalização de modelos estruturais de arquiteturas ROS, e especificações comportamentais dos seus nodos em Electrum. Após formalização do sistema, as propriedades são verificadas através de técnicas de model-checking. De forma a automatizar a análise, a técnica descrita neste documento é implementada através de um plug-in para HAROS, uma framework utilizada no control de qualidade de software ROS. A técnica proposta, assim como a sua implementação sobre o ambiente Haros, foram positivamente avaliadas aquando da sua aplicação em um caso real, AgRobV16. Um robô agrícola, cuja dimensão e complexidade são representativos daquilo que seria de esperar em verdadeiros ambientes industriais.