Publicação
Analysis of message passing software using electrum
| Resumo: | 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. |
|---|---|
| Autores principais: | Carvalho, Bruno Renato Fernandes |
| Assunto: | Software verification Model checking Safety Robotics Electrum ROS HAROS Verificação de software Robótica Engenharia e Tecnologia::Engenharia Eletrotécnica, Eletrónica e Informática |
| Ano: | 2020 |
| País: | Portugal |
| Tipo de documento: | dissertação de mestrado |
| Tipo de acesso: | acesso aberto |
| Instituição associada: | Universidade do Minho |
| Idioma: | inglês |
| Origem: | RepositóriUM - Universidade do Minho |
| Resumo: | 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. |
|---|
Atividades financiadas
Não foram encontrados projetos financiados.