Applying formal verification techniques to embedded software in UAV design

Abstract

O desenvolvimento de sistemas considerados safety-critical, como no caso dos Veículos Aéreos Não-Tripulados (VANTs), é uma tarefa que exige altos níveis de garantia dos requisitos funcionais e não funcionais previstos em seu projeto. Devido a complexidade desses sistemas, que envolvem muitas funcionalidades e constante interação com o ambiente externo, onde uma falha em sua operação pode ocasionar consequências graves, a utilização de técnicas de verificação são imprescindíveis para validação desses requisitos, visto que propriedades que descrevem o correto funcionamento do sistema alvo são confrontadas com seu modelo atual. Apesar da existência de técnicas eficientes na verificação, muitas vezes a necessidade de complementar essa abordagem é fundamental para cobrir alguns gargalos deixados por limitações existentes e assegurar a corretude do sistema. Nesse sentido, muitos esforços por parte das comunidades e empresas foram realizados na integração desses métodos de verificação, porém isto ainda é um grande desafio. Com isto, um processo de verificação que envolve técnicas como model checking, runtime verification e análise do comportamento do software são previstas na proposta deste trabalho. Com intuito de aplicar essa abordagem, um projeto de Veículo Aéreo Não Tripulado (VANT) é utilizado como caso de estudo, na qual o foco principal é a validação do escalonamento de tarefas do software envolvido.

Abstract: The development of safety-critical systems, as in the case of Unmanned Aerial Vehicles (UAVs), is a task that requires high levels of assurance of the functional and non-functional requirements expected in its project. Due to the complexity of these systems, which involve many functionalities and constant interaction with the external environment, where a failure in its operation can cause serious consequences, the use of verification techniques are crucial to validate these requirements, since properties that describe the correct functioning of the target system are confronted with its current model. Despite the existence of efficient verification techniques, often the need to complement this approach is fundamental to cover some gaps left by existent limitations and ensure system correctness. In this sense, many efforts by communities and companies have been made in integrating these verification methods, but this is still a great challenge. With this, a verification process involving techniques like model checking, runtime verification and analysis of software behavior are foreseen in the proposal of this work. In order to apply this approach, a UAV project is used as a case study, where the main focus is to validate the scheduling problem of the involved software.