Formal verification toolchain using ESBMC, FRET, and R2U2 for improving the reliability of two critical embedded system

Abstract

Sistemas Críticos de Segurança (SCS) são sistemas que exigem um alto nível de confiabilidade. Ferramentas de Verificação Formal (FV) são utilizadas para atender a essa necessidade de alta confiabilidade, minimizando a possibilidade de problemas. No entanto, muitas ferramentas de FV são usadas apenas para fins acadêmicos e não são amplamente adotadas no mercado. Diante desse contexto, esta Dissertação de Mestrado propõe uma cadeia de ferramentas chamada de Cadeia de Ferramentas para Formalização, Análise em Tempo de Execução e Avaliação de Código (FRACET), que se concentra na aplicação de ferramentas de verificação formal para aprimorar a confiabilidade de dois SCS: o portfólio eSEA da Bosch Rexroth e o projeto ProVANT UAV. Ambos os sistemas operam em ambientes de alto risco, onde falhas podem levar a consequências graves, classificando-os como SCS. O estudo também tem como objetivo avaliar o desempenho das ferramentas utilizadas no processo. O método emprega o ESBMC para análise estática de código a fim de identificar vulnerabilidades, o FRET para formalizar e refinar requisitos, e o R2U2 para verificação em tempo de execução, garantindo a conformidade com as especificações. Os resultados foram avaliados com base no que era esperado de cada ferramenta e em sua relevância para os cenários aplicados. Após a criação de uma configuração para cada ferramenta e sua aplicação em ambos os cenários, concluiu-se que cada ferramenta teve um bom desempenho, fornecendo diagnósticos precisos e detectando várias vulnerabilidades nos dois casos de estudo. Para a Rexroth, a análise identificou vulnerabilidades, atualizou requisitos desatualizados e validou a conformidade com as especificações em cenários críticos, fornecendo insights acionáveis para a equipe da Rexroth. Da mesma forma, no projeto ProVANT, as ferramentas revelaram vulnerabilidades, refinaram requisitos e demonstraram a viabilidade da verificação em tempo de execução, apesar das limitações de hardware. A principal contribuição da tese reside na integração inovadora dessas ferramentas em uma metodologia coesa, aplicável em diversos domínios (subaquático e aeroespacial), e na ênfase na automação, que aumenta a eficiência e a escalabilidade. No geral, o trabalho alcançou com sucesso seu objetivo de avaliar a confiabilidade dos sistemas e o desempenho das ferramentas, oferecendo insights valiosos para a melhoria de pipelines de desenvolvimento em sistemas críticos de segurança.

Abstract: Safety-Critical Systems (SCS) are systems that require a high level of reliability. Formal Verification (FV) tools are used to address this necessity of high reliability to minimize the possibility of any issues. However, many FV tools are only used for academic purposes and are not widely used on the market. Given this context, this master's thesis proposes a toolchain called Formalization, Runtime Analysis, and Code Evaluation Toolchain (FRACET), which focuses on applying formal verification tools to enhance the reliability of two SCS: the eSEA portfolio from Bosch Rexroth and the ProVANT UAV project. Both systems operate in high-stakes environments where failures could lead to severe consequences, classifying them as SCS. The study also aims to evaluate the performance of the tools used in the process. The method employs ESBMC for static code analysis to identify vulnerabilities, FRET for formalizing and refining requirements, and R2U2 for runtime verification to ensure adherence to specifications. The results were evaluated based on what was expected of each tool and their relevance to the applied scenarios. After creating a setup for each tool and testing them in both scenarios, it was concluded that each tool performed well, giving precise diagnostics and detecting several vulnerabilities in both case studies. For Rexroth, the analysis identified vulnerabilities, updated obsolete requirements, and validated adherence to specifications in critical scenarios, providing actionable insights for Rexroth's team. Similarly, in the ProVANT project, the tools uncovered vulnerabilities, refined requirements, and demonstrated the feasibility of runtime verification despite hardware limitations. The thesis's main contribution lies in its innovative integration of these tools into a cohesive method, applicable across diverse domains (subsea and aerospace), and its emphasis on automation, which enhances efficiency and scalability. Overall, the work successfully achieved its goal of assessing system reliability and tool performance, offering valuable insights for improving development pipelines in safety-critical systems.