Publicado no Encontro de Saberes 2017
Evento: XXV 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 logica temporal linear para teste baseado em propriedades de sistemas embarcados |
| Autores |
|
MATHEUS TAKESHI YAMAKAWA IKEDA (Autor) Elton Maximo Cardoso (Orientador) |
| Resumo |
| A tecnologia tornou-se indiscutivelmente essencial e presente na vida de todos. Vemos cada vez mais sistemas computadorizados participando de processos a fim de otimizar tempo e precisão, entre outras variáveis, e/ou diminuir custos. As aplicações são diversas e em muitas áreas, não só restrita à ambientes industriais, já em aparelhos comuns ao uso de muitos. A segurança e credibilidade dos sistemas são fundamentais para a seu completo funcionamento e para próximas versões, e para garantir a ausência de erros, os mesmos são submetidos a testes convencionais e simulações, todavia, a construção e execução destes são responsáveis por 50% do custo do desenvolvimento. Este projeto teve como proposta a criação de uma biblioteca para teste baseado em propriedades para sistemas embarcados, utilizando lógica temporal para especificação de propriedades destes sistemas, geradores de valores de teste e uma linguagem de domínio específico que permita o desenvolvimento destes sistemas para evitar problemas comuns decorrentes do uso de linguagens de baixo nível como C/C++, que são as mais utilizadas neste tipo de domínio de aplicações. Obtivemos como resultado a implementação de um teste de satisfazibilidade de fórmulas da LTL na linguagem funcional. Basicamente, uma função recursiva e um novo tipo de dados nomeado LTL, no qual implementamos a sintaxe, isto é, todos os conectivos e operadores presente neste tipo de lógica. Dentre os objetivos deste projeto, estava a implementação de uma linguagem de domínio específico embarcada imperativa para desenvolvimento de dispositivos embarcados para programação segura em C. Foi projetado uma representação de uma árvore sintática abstrata a qual contém representações de elementos presentes na linguagem imperativa C, como declarações, , funções, operadores lógicos e aritméticos para posteriormente uma especificação de uma DSL a qual contém, para um primeiro momento, declarações de funções que representam laços, condições if-else, etc. |
