Publicado no Encontro de Saberes 2016
Evento: XXIV Seminário de Iniciação Científica
Área: CIÊNCIAS EXATAS E DA TERRA
Subárea: Ciência da Computação
Órgão de Fomento: Universidade Federal de Ouro Preto
| Título |
| Uso de lógica temporal linear para teste baseado em propriedades de sistemas embarcados. |
| Autores |
|
MATHEUS TAKESHI YAMAKAWA IKEDA (Autor) RODRIGO GERALDO RIBEIRO (DECSI) (Orientador) |
| Resumo |
| Testes são 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 dispensiosa, responsável por cerca de 50% do custo do desenvolvimento de um sistema. Isso motiva o estudo de técnicas para a automação completa ou parcial de testes. Neste sentido, diversas técnicas para automação de testes foram propostas na literatura. Uma destas é o chamada de teste baseado em propriedades, em que valores para teste são produzidos de forma automática e verificados com respeito a propriedades descritas como fórmulas da lógica de primeira ordem. 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 dispositivos médicos. Sistemas embarcados são normalmente implementados como sistemas reativos, isto é, programas cuja execução é acionada mediante a existência de ``estímulos'' do ambiente externo como, por exemplo, a leitura de um certo valor em um sensor. Por sua execução ser determinada por eventos externos, testar sistemas embarcados é uma tarefa complexa. 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. Neste sentido, o presente projeto desenvolveu técnicas para teste baseado em propriedades descritas utilizando lógica temporal e sua aplicabilidade no teste de sistemas embarcados. Como resultado, um protótipo de uma ferramenta para testes baseado em propriedades usando a lógica linear temporal foi desenvolvida e um interpretador de uma linguagem para a plataforma Arduíno está sendo desenvolvido para integração com a ferramenta de testes proposta. |
