Runtime Verification of Low-Level Software in a VTOL UAV

Abstract

In Safety-Critical Systems (SCS), it is a difficult task to ensure the correctness of the software implementation. Therefore, formal verification techniques sound like an interesting solution. ProVANT, a project that targets developing an Unmanned Aerial Vehicle (UAV), a typical SCS, can benefit from such techniques. In this respect, the present work focuses on Runtime Verification (RV), which serves to formally verify the systems requirements, online, in real-time, or offline using obtained trace data. The Realizable, Responsive, Unobtrusive Unit (R2U2) framework, developed by NASA and Iowa State University, is applied in this work to verify the software of the Low-Level control system of the UAV under design in the ProVANT project. The original project requirements were revised and adapted with the intent of applying them in RV. Different categories were identified in the already existing requirements, and they served as a basis for a hierarchical way to define new requirements. The requirements were written in the Formal Requirements Elicitation Tool (FRET), and Temporal Logic formulas were automatically generated and exported by the FRET software. A subset of formulas were then selected for validation of the framework, running the verification on the same intended hardware in an emulated network with different hardware. Some of the properties were verified, and the verification program’s resource usage was measured and analyzed.

Em sistemas críticos para a segurança (Safety-Critical Systems, ou SCS em inglês), é uma tarefa difícil garantir a exatidão da implementação de código. Portanto, técnicas de verificação formal aparentam ser boas soluções. O ProVANT, um projeto empenhado no desenvolvimento de um Veículo Aereo Não Tripulado (VANT), um típico SCS, pode se beneficiar de tais tecnicas. Nesse respeito, o presente trabalho foca Verificação em Tempo de Execução (Runtime Verification, em inglês), que serve para verificar formalmente requisitos de um sistema, online, em tempo real, ou offline, usando um registro de uma execução extraído do programa. O Realizable, Responsive, Unobtrusive Unit (Unidade Realizável, Responsiva e Não-intrusiva, ou R2U2), desenvolvido pela NASA e a Universidade Estadual de Iowa, é aplicado nesse trabalho para verificar o programa do controlador de baixo-nível do VANT do ProVANT. Os requisitos originais do projeto foram revisados e adaptados com o proposito de serem aplicados na Verifcação em Tempo de Execução. Categorias de requisitos diferentes foram encontradas nos requisitos já existentes, que serviram de base para uma abordagem hierárquica para a definição de novos requisitos. Esses requisitos foram escritos em FRET (Formal Requirements Elicitation Tool, ou Ferramenta de Elicitação de Requisitos Formais, em português), e as fórmulas de Lógica Temporal foram automaticamente geradas e exportadas pelo aplicativo FRET. Um subconjunto de fórmulas foi selecionado para a validação do programa, rodando a verificação na mesma máquina embarcada usada no projeto, em uma rede emulada com máquinas diferentes. Algumas das propriedades foram verificadas e o consumo de recursos do programa de verificação foi medido e analisado