Detalhes bibliográficos
| Ano de defesa: |
2011 |
| Autor(a) principal: |
Rhenzo Losso |
| Orientador(a): |
Não Informado pela instituição |
| Banca de defesa: |
Não Informado pela instituição |
| Tipo de documento: |
Dissertação
|
| Tipo de acesso: |
Acesso aberto |
| Idioma: |
por |
| Instituição de defesa: |
Instituto Tecnológico de Aeronáutica
|
| Programa de Pós-Graduação: |
Não Informado pela instituição
|
| Departamento: |
Não Informado pela instituição
|
| País: |
Não Informado pela instituição
|
| Palavras-chave em Português: |
|
| Link de acesso: |
http://www.bd.bibl.ita.br/tde_busca/arquivo.php?codArquivo=1962
|
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. |
