60ª Reunião Anual da SBPC

INTRODUÇÃO:

Um dos principais desafios no domínio de sistemas embarcados é verificar a corretude lógica e temporal do software embarcado (ESW). Neste trabalho proposto, foi utilizada uma abordagem de geração de “mutantes” para verificação de especificações de projeto e posteriormente obter a geração de testes utilizando a ferramenta Model-Checking. Esta ferramenta utiliza a linguagem CFA (Communicating Finite Automata) para descrever a especificação do sistema e CTL (Computational Tree Logic) para descrever as propriedades do sistema. A prática atual na indústria consiste basicamente em implementar uma dada especificação em uma linguagem de programação que seja a mais conveniente para o sistema em questão. No entanto, este processo manual de codificação da especificação, pode ocasionar erros severos ao ESW tais como erros de estouro da memória/pilha, cálculos envolvendo ponto flutuante, deadlock, e temporais. Sendo assim, este trabalho consiste em automatizar a geração de casos de teste a partir de um modelo especificado em CFA com o intuito de garantir uma melhor confiabilidade e reduzir os custos relacionados ao teste do sistema.

METODOLOGIA:

O trabalho realizado baseia-se na especificação do software para geração de “mutantes”. Tendo certeza de que o modelo é correto, será feita uma busca no modelo original alterando flags e transições que são necessários para o funcionamento, caso após as mudanças o modelo “mutante” funcione corretamente há algo de errado com o modelo original, do contrário serão gerados o contra-exemplo. O contra-exemplo é uma indicação da ferramenta utilizada na verificação de propriedades (Model-Checking), que mostra quais estados foram testados, sabendo assim onde ocorreu o erro. Essa abordagem foi utilizada, pois para um sistema pequeno o número de “mutantes” também é pequeno, mas à medida que aumenta os estados, os “mutantes” aumentarão. O número de “mutantes” será finito, visto que o número de estados é finito, mas esse número pode crescer muito gerando uma explosão combinatória. Esse método reduz o número de modificações a serem realizadas, pois se o sistema está baseado em uma especificação é necessário que ele funcione dessa maneira, não necessitando que se faça casos de teste fora da especificação. A continuação dos testes consiste em verificar propriedades em cada “mutante” e verificar os resultados, como correto ou geração do contra-exemplo que indica falha no modelo.

RESULTADOS:

Os resultados obtidos foram baseados no algoritmo de exclusão mútua de Dekker, com esse algoritmo foi gerado um modelo, depois de o modelo pronto foi gerado um autômato para visualizar melhor a especificação do projeto. Com o autômato criado foi verificada cada transição do modelo para retirar as especificações, depois de feito isso foi criada uma tabela representando cada transição com sua devida especificação do que deveria ocorrer para habilitar a transição, com esses dados foi gerado um “mutante” para cada especificação, ou seja, foi causado um erro em cada especificação para poder gerar as verificações de propriedades e observar o comportamento do modelo. A verificação de propriedade, neste caso, foi o teste de alcançabilidade, ou seja, se um estado x é alcançável partindo de um estado y. Se a resposta a este teste fosse positiva quando verificado no modelo “mutante” indicaria falha no modelo original, pois as especificações foram alteradas, para o caso de resposta negativa o modelo está respeitando as especificações. Nesse teste foram gerados 27 “mutantes”, que manualmente gastou um dia, no computador foi questão de minutos, e na realização da verificação de propriedade todos passaram no teste, então como era esperado o algoritmo de exclusão mútua não apresenta falha.

CONCLUSÕES:

As conclusões que podem ser tiradas é que, a abordagem utilizada além de dar maior confiabilidade para o projeto, visto que está se baseando na própria especificação, agiliza o processo, pois criar os “mutantes” manualmente demora muito mais tempo do que usar o computador para essa geração. É possível observar que com um modelo original e suas especificações de funcionamento a geração de testes para garantir sua funcionalidade se realizará em menos tempo e com maior precisão, este resultado garantirá maior velocidade de geração de testes e com isso menor custo no desenvolvimento do projeto. Podendo ter uma maior confiabilidade no resultado final do projeto, essa abordagem se encaixa perfeitamente para a geração de testes para sistemas embarcados de tempo-real, onde é necessária grande precisão ao garantir que o projeto está livre de erros.

Instituição de fomento: CNPQ - Conselho Nacional de Desenvolvimento Científico e Tecnológico

Trabalho de Iniciação Científica

Palavras-chave: Sistemas Embarcados, Geração de testes, Model-checking

E-mail para contato: cesroceng@dcc.ufam.edu.br