Especificação de requisitos usando TLA + e métodos formais no modelo de sistema de orientação de voo na Nasa.

Abstract

RESUMO: O contexto deste trabalho é a necessidade de trazer maior segurança e prevenir as falhas potenciais na utilização de veículos aéreos não tripulados “VANTs” em atividades e serviços em conglomerados habitados. Com esse objetivo em mente, verificou-se a oportunidade de se buscar a experiência com a aplicação de métodos formais em sistemas de software da aviação comercial convencional visando identificar o que precisa e deve ser futuramente aplicado em sistemas de orientação de voo aplicados em VANTs. O trabalho foi iniciado tomando-se como base a especificação de um sistema de orientação de voo, estabelecido pela NASA - National Aeronautics and Space Administration, em sua versão original, escrita na linguagem RSML−e- Requirements State Machine Language sem transmissão interna de eventos. Posteriormente, a versão da especificação do sistema de orientação de voo desenvolvida em notação Z, no âmbito da própria NASA, também foi utilizada como referência para a realização das especificações do Flight Guidance System - FGS, em TLA+. O presente trabalho concentrou-se nos documentos que embasaram a especificação original do FGS da NASA. O estudo foi concentrado nas linguagem TLA+, RSML−ee na Notação Z assim como na estruturação do uso de métodos formais em sistemas aplicados em aviação pela NASA, focando nos requisitos para homologação de sistemas, no método CoRE, e nos demais documentos referenciados nestes. Foram escritas especificações em TLA+para os eventos de entrada e termos da especificação formal em Z. Os eventos foram especificados e verificados individualmente e depois em conjunto com os demais. Finalmente focou-se no modo lógico do sistema de orientação de voo - FGS, com base na especificação original em RSML−e, especificou-se cada um dos modos de voo individualmente e foi realizada a verificação correspondente. Em seguida agrupou-se as especificações dos modos de voo e foi realizada a verificação de propriedades e invariantes que devem ser preservadas e atendidos ao longo dos diversos estados assumidos nos modelos.

ABSTRACT: The context of this work is the need of bring greater safety and prevent potential failures in the use of unmanned aerial vehicles (UAV) in activities and services on inhabited conglomerates. With this objective in mind, it was verified the opportunity of seek for experience with the application of formal methods in conventional commercial aviation software systems in order to identify what it is necessary to be applied in future development of flight guidance systems for UAV’s. This work has started taking as base the flight guidance system specification, developed by NASA - National Aeronautics and Space Administration, from original version, written in RSML−e- Requirements State Machine Language without any internal broadcast of events. In the sequence, the flight guidance system specification written in Z notation, sponsored by NASA, also it was used as reference to write the TLA+specifications of the Flight Guidance System - FGS. This work has focused on the documents refered in the original specification of the FGS, and it was concentrated on the languages TLA+, RSML−e, and on Z Notation as well as on the structured formal methods methodology applied for development of avionics systems by NASA, with special attention on requirements for certification, and on CoRE method, considering all the others documents referenced by them. Spefifications were written in TLA+for input events and terms listed in the flight guidance formal Z specification. Each one of the input events was specified and verified separetely and subsequently with all the others together. Finally the work was focused on the logic mode of the flight guidance system - FGS, taking the original specification as reference, specifying each one of the flight modes individually, and verifying it. Subsequently the flight modes specifications were grouped in order to verify some properties and invariants that should be preserved for every state when running all the models together