skip to main content
Idioma:

Especificação e verificação formal de requisitos para sistemas de tráfego aéreo.

Aguchiku, Fábio Seiti

Biblioteca Digital de Teses e Dissertações da USP; Universidade de São Paulo; Escola Politécnica 2018-08-03

Acesso online. A biblioteca também possui exemplares impressos.

  • Título:
    Especificação e verificação formal de requisitos para sistemas de tráfego aéreo.
  • Autor: Aguchiku, Fábio Seiti
  • Orientador: Maruyama, Newton
  • Assuntos: Lógica Temporal; Métodos Formais; Sistemas Críticos; Tráfego Aéreo (Automação; Gerenciamento); Air Traffic Management Systems; Formal Methods; Safety-Critical System; Temporal Logic
  • Notas: Dissertação (Mestrado)
  • Notas Locais: Programa Engenharia Mecânica
  • Descrição: A evolução de sistemas de gerenciamento de tráfego aéreo é pesquisada para suportar o crescimento na demanda por transporte aéreo. Uma alternativa para essa evolução é o aumento no grau de automação. Os sistemas automatizados precisam ser tão seguros quanto os sistemas em operação atualmente. Com o uso de técnicas de especificação e verificação formal é possível avaliar os requisitos de sistemas. Neste trabalho, é proposto um ciclo de especificação formal, que consiste em um conjunto de diretrizes para aplicação de técnicas de métodos formais em requisitos escritos em linguagem natural. O resultado esperado da aplicação deste ciclo é um conjunto de requisitos escritos em linguagem natural verificados formalmente. O ciclo é composto pelas etapas: levantamento de requisitos do sistema e classificação em padrões de especificação; mapeamento dos requisitos para as linguagens de especificação formal LTL (Linear Temporal Logic) e CTL (Computation Tree Logic); verificação formal da especificação com o verificador NuSMV; ajustes na especificação baseada nos resultados da verificação; ajustes nos requisitos baseados nos ajustes na especificação. As diretrizes propostas são definidas com a análise da verificação formal do Automated Airspace Concept (AAC), padrões de especificação e diretrizes para uso do verificador NuSMV. Os resultados esperados são obtidos na aplicação do ciclo de especificação em dois estudos de caso. A principal contribuição do trabalho é o conjunto de diretrizes para elaboração de expressões escritas em linguagem de especificação formal baseadas em requisitos escritos em linguagem natural e que podem ser verificadas formalmente.
  • DOI: 10.11606/D.3.2018.tde-04102018-135028
  • Editor: Biblioteca Digital de Teses e Dissertações da USP; Universidade de São Paulo; Escola Politécnica
  • Data de criação/publicação: 2018-08-03
  • Formato: Adobe PDF
  • Idioma: Português
Links
Voltar para lista de resultados
Ir para página anteriorAnterior Resultado  10 AvançarIr para próxima página

  • Realização: ABCD-USP USP   Logos de Redes Sociais: Freepik

Buscando em bases de dados remotas. Favor aguardar.