Show simple item record

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

dc.contributor.advisorAndrade, Jefferson Oliveira
dc.contributor.authorCurátola, Olavo José Ferreira
dc.date.accessioned2022-01-25T14:34:48Z
dc.date.available2022-01-25T14:34:48Z
dc.date.issued2021
dc.identifier.citationCurátola, Olavo José Ferreira Especificação de requisitos usando TLA + e métodos formais no modelo de sistema de orientação de voo na Nasa. 146 f. 2021. Monografia (Graduação em Sistemas de Informação) - Instituto Federal do Espírito Santo, Serra, 2021.pt_BR
dc.identifier.urihttps://repositorio.ifes.edu.br/handle/123456789/1536
dc.description.abstractRESUMO: 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.pt_BR
dc.description.abstractABSTRACT: 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 togetherpt_BR
dc.format.extent146 f.pt_BR
dc.languagept_BRpt_BR
dc.rightsacesso_abertopt_BR
dc.subjectEspecificação Formal.pt_BR
dc.subjectModelagem de Sistemas.pt_BR
dc.subjectLinguagem TLA +pt_BR
dc.subjectFormal Methods.pt_BR
dc.subjectFormal Specification.pt_BR
dc.subjectFlight Guidance System.pt_BR
dc.subjectTLA + Language.pt_BR
dc.subjectDronept_BR
dc.subjectMétodos formais (Ciência da Computação)pt_BR
dc.subjectSistemas de guiagem (Flight)pt_BR
dc.subjectSoftware - Desenvolvimentopt_BR
dc.titleEspecificação de requisitos usando TLA + e métodos formais no modelo de sistema de orientação de voo na Nasa.pt_BR
dc.typetccpt_BR
dc.publisher.localSerrapt_BR
ifes.campusCampus_Serrapt_BR
ifes.advisor.latteshttp://lattes.cnpq.br/7138275599443632pt_BR
ifes.course.undergraduateBacharelado em Sistemas de Informação
dc.contributor.memberKomati, Karin Satie
dc.contributor.memberSouza, Flávio Severiano Lamas de
ifes.member.latteshttp://lattes.cnpq.br/9860697624155451pt_BR
ifes.member.latteshttp://lattes.cnpq.br/9220596355621571pt_BR
ifes.member.orcidhttps://orcid.org/0000-0001-5677-4724pt_BR
ifes.advisor.orcidhttps://orcid.org/0000-0002-5321-9239pt_BR


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record