PG-EAM - Programa de Pós-Graduação em Engenharia Aeronáutica e Mecânica
EN PT
Dissertação de Mestrado 2009

Estudo da verificação e validação de sistemas embarcados espaciais utilizando SysML e Model Checking.

Autor

Eduardo Correia da Silva

Orientador

Área de Concentração

Sistemas Aeroespaciais e Mecatrônica

Data de Defesa

18/09/2009

Número da Tese

000555681

Resumo

Entre as principais dificuldades do desenvolvimento de software embarcado crítico e de tempo real está a especificação e o processo de verificação e validação apoiado ao projeto conceitual. Neste contexto, a modelagem de sistemas tem uma importante função, uma vez que um processo complexo possa ser analisado e validado antes de sua real implementação. Esta dissertação aborda o problema de verificação e validação de software embarcado de um satélite com configuração ACDH (Attitude Control and Data Handling) através de uma plataforma aerosuspensa com um grau de liberdade, utilizando a SysML, a ferramenta CASE TELELOGIC Rhapsody e a orientação das normas da ECSS (European Cooperation on Space Standardization). A partir do modelo obtido, são utilizadas três abordagens para análise e avaliação: (1) Especificação e gerenciamento dos requisitos, através dos conceitos determinados pela ECSS; (2) Modelagem do sistema e verificação dos requisitos, através do formalismo matemático dos autômatos utilizando a técnica de model checking através da ferramenta UPPAL; (3) Conversão do modelo em SysML, aplicando a Engenharia de Requisitos e o processo de verificação e validação do sistema, através da simulação na ferramenta CASE.

Palavras-chave

Sistemas de computadores embarcados Especificação formal Verificação de programas (computadores) Verificação formal Ferramentas de desenvolvimento de software Software de segurança crítica Teoria dos autômatos Engenharia de software