Um estudo do uso do java Pathfinder na verificação e validação de softwares espaciais

• Processo: 12/16913-2
• Modalidade de apoio: Bolsas no Brasil - Iniciação Científica
• Data de Início da vigência: 01 de dezembro de 2012
• Data de Término da vigência: 30 de novembro de 2013
• Área de conhecimento: Ciências Exatas e da Terra - Ciência da Computação
• Pesquisador responsável: Ana Cristina Vieira de Melo
• Beneficiário: Camila Fernandez Achutti
• Instituição Sede: Instituto de Matemática e Estatística (IME). Universidade de São Paulo (USP). São Paulo , SP, Brasil
• Assunto(s): Softwares Desenvolvimento de software Java Gestão da segurança em sistemas computacionais Validação de programas de computador
• Palavra(s)-Chave do Pesquisador: Java Pathfinder | software crítico | validação | verificação | Verificação e Validação de Softwares

Resumo

Existe atualmente uma crescente preocupação mundial com a qualidade dos softwares, sendo ele crítico ou não, já que a evolução dos sistemas computacionais aumentou exponencialmente e, portanto, as funcionalidades implementadas neles são cada vez mais completas e complexas, exigindo que o desenvolvedor e o cliente confiem na correção completa do projeto. Outro motivo para tamanha preocupação são os grandes investimentos na melhoria dos processos de desenvolvimento de software. Quando tratamos de softwares críticos essa preocupação é ainda maior. Sendo assim, o investimento em técnicas para validação e verificação de softwares é cada vez maior e imprescindível. Esse projeto vem então explorar a temática da qualidade de softwares em sistemas críticos fazendo o estudo e aplicação de métodos de verificação sobre um sistema real da área espacial. Nesse projeto, um estudo sobre a especificação formal de um sistema crítico será realizada para então desenvolver a implementação do projeto na linguagem Java e aplicar técnicas de verificação sobre o sistema desenvolvido. Para tanto, o verificador de modelos, desenvolvido pela NASA, será utilizado já que ele tem sido amplamente desenvolvido pela comunidade científica e aplicado a problemas críticos. O caso real a ser desenvolvido será um software embarcado espacial, pois a necessidade de verificação e validação é ainda mais intensificada quando se trata de sistemas espaciais. Visando, assim explorar todos os passos de uma verificação apropriados para um software de missão crítica. Os resultados deste trabalho têm aplicação direta no mundo real e, principalmente nos projetos de programas de coleta e análise de dados espaciais.(AU)