Teste de software baseado em lógica temporal linear em sistemas reativos.

Abstract

Testes são certamente a abordagem mais utilizada por desenvolvedores de todo o mundo para a garantia da qualidade de software. Porém, a construção e execução de testes é uma atividade dispendiosa, responsável por cerca de 50% do custo do desenvolvimento de um sistema. Atualmente, sistemas embarcados são ubíquos na sociedade moderna e estão presentes nos mais diversos dispositivos eletrônicos onde a corretude e segurança são fatores críticos, como aplicações bancárias e dispositivos médicos. Por sua execução ser determinada por eventos externos, testar sistemas embarcados é uma tarefa complexa, sendo muitas vezes feita com o sistema em produção, o que pode acarretar o aumento do custo do desenvolvimento do software. Além das dificuldades para construção de testes, sistemas reativos não são facilmente especificados utilizando fórmulas da lógica de primeira ordem, uma vez que esta não possui mecanismos para representar, de forma simples, a relação temporal entre ações do sistema.Tais formulações são feitas de maneira natural utilizando as chamadas lógicas temporais, em que a noção de tempo é explícita na semântica de fórmulas. O presente trabalho representa uma contribuição tecnológica por fornecer, a desenvolvedores de sistemas embarcados, uma técnica moderna para a validação de software, com a implementação de uma ferramenta para teste baseado em propriedades descritas utilizando lógica temporal e uma linguagem de domínio especifico embarcada imperativa para a programação segura nas linguagens correntes para o desenvolvimento destes sistemas. Para verificar a usabilidade da ferramenta desenvolvida, realizaram-se testes com escopos simples, próximos aos programadores, como o controle de dois semáforos sincronizados e a leitura de um sensor de temperatura, nos quais possíveis propriedades temporais foram especificadas e testadas, a fim de se observar a validação delas diante dos algoritmos testados.