Contribuições do model checking e da metodologia CoFi para o software embarcado espacial.

AUTOR(ES)

Rodrigo Pastl Pontes

FONTE

IBICT - Instituto Brasileiro de Informação em Ciência e Tecnologia

DATA DE PUBLICAÇÃO

11/02/2011

RESUMO

A crescente participação do software embarcado nas causas dos últimos acidentes espaciais evidencia a importância dos processos e técnicas de verificação e validação no desenvolvimento do software embarcado espacial. Neste contexto, este trabalho investiga a contribuição de duas técnicas de verificação para aplicações espaciais. A primeira técnica é o model checking baseado no uso da ferramenta UPPAAL. O UPPAAL adota a modelagem do sistema em autômatos temporizados e permite a verificação de propriedades especificadas em um subconjunto da linguagem CTL (Computational Tree Logic). A segunda técnica consiste especificação e aplicação de testes a partir de modelos de estados, considerando mais especificamente a metodologia CoFI (Conformance and Fault Injection). São utilizados como estudo de caso dois produtos de software espacial. Um dos produtos foi desenvolvido com o uso do model checking, enquanto o outro foi desenvolvido de acordo com as práticas atualmente aplicadas pelo grupo de computador de bordo do Departamento de Eletrônica Aeroespacial do INPE (Instituto Nacional de Pesquisas Espaciais). Ambos os produtos de software foram testados utilizando a metodologia CoFI. Cada produto consiste de uma implementação de dois serviços especificados na norma europeia PUS (Packet Utilization Standard). Estes serviços representam funcionalidades oferecidas por um computador de gerenciamento de bordo de satélites. As principais conclusões obtidas são que a metodologia CoFI contribui para o aprimoramento dos processos de verificação atualmente em uso no INPE, e que, o model checking associado à geração manual do código não implica na ausência de erros, porém ajuda a reduzir o número, mas não a criticidade de erros quando comparado com as práticas atualmente em uso.

ASSUNTO(S)

sistemas de computadores embarcados verificação de programas (computadores) desenvolvimento de software testes de programa veículos espaciais engenharia de software engenharia aeroespacial

Documentos Relacionados

• Contribuições do model checking e da metodologia CoFi para o software embarcado espacial.
• Metodologia para padronização no processo de correção geométrica para imagens orbitais de média resolução espacial.
• Metodologia de projeto de software embarcado voltada ao teste
• Metodologia de determinação do banco de sementes de plantas daninhas para confecção de mapas de distribuição espacial.
• CERTIFICAÇÕES E INDICADORES SOCIOAMBIENTAIS: RELAÇÃO, DISCURSO E VALOR DA MATERIALIZAÇÃO ESPACIAL.