| Título: | Modelagem e verificação formal do software embarcado de um simulador de satélite |
| Autor: | Rhenzo Losso |
| Programa: | Engenharia Aeronáutica e Mecânica |
| Área de Concentração: | Sistemas Aeroespaciais e Mecatrônica |
| Orientador : | Emilia Villani |
| Coorientador : | Osamu Saotome |
| Ano de Publicação : | 2011 |
| Curso : | Mestrado Acadêmico |
| Assuntos : | Sistemas de computadores embarcados |
| t | Verificação formal |
| t | Verificação de programa (computadores) |
| t | Satélites |
| t | Veículos aeroespaciais |
| t | Engenharia de software |
| Resumo : | Este trabalho tem como objetivo a análise da aplicação de métodos formais para a modelagem e verificação de produtos de software embarcado para aplicações aeroespaciais de tempo-real. Como abordagem para modelagem, utilizam-se autômatos temporizados e a ferramenta UPPAAL. A verificação do modelo construído é realizada por meio da abordagem de model-checking, utilizando um conjunto de propriedades definidas em CTL que refletem os requisitos do sistema em análise. Particular ênfase é dada ao problema de verificação de requisitos de tempo no sistema em análise. Para tanto, a metodologia proposta inclui a modelagem não apenas do aplicativo de software mas também do sistema operacional que gerencia os diversos processos executados pelo software. Como estudo de caso utiliza-se o computador de bordo de um simulador de satélite com um grau de liberdade. Este estudo de caso inclui a determinação dos tempos utilizados para execução do software aplicativo e dos tempos utilizados pelo sistema operacional. Além da verificação dos requisitos de tempo do sistema, o estudo de caso apresenta uma análise de sensibilidade destes requisitos frente à variação de alguns parâmetros do sistema. Baseado nos resultados do estudo de caso, apontam-se as vantagens e limitações do uso da abordagem de model checking para verificação de sistemas de tempo real para aplicações aeroespaciais. |
| Data de Defesa : | 14/12/2011 |
| Texto na íntegra : | [Visualizar] |