Validação de uma especificação TDevC para o desenvolvimento de device drives robustos

Abstract

O uso de sistemas eletrônicos embarcados está cada vez mais presente no dia a dia da sociedade. Telefones celulares,sistemas de posicionamento global (GPS) e televisores digitais com telas de LCD são exemplos de equipamentos que estão incorporando funcionalidades para atender às demandas dos usuários, e, consequentemente, aumentando a complexidade dos sistemas embarcados nesses dispositivos. De fato, a grande maioria das inovações em sistemas embarcados é atribuída aos avanços na microeletrônica e no projeto de software embarcado. Porém, devido a atual complexidade dos dispositivos, projetos de hardware não conseguem acompanhar o crescimento da capacidade física do hardware, havendo um gap de produtividade entre o desenvolvimento do hardware e o desenvolvimento do software necessário para a sua operação. Esses softwares, também conhecidos como Software dependente do Hardware (Hardware-dependent Software - HdS ), estão no centro do desafio do projeto de sistemas. Dentre esses HdS, pode-se citar os device drivers ou drivers dos dispositivos. Os drivers são codificados com base na documentação disponível pelos fornecedores do hardware, porém, na maioria das vezes, esse documento não é de fácil leitura, podendo levar a erros de interpretação. Atrelado a isso, como essa documentação está escrita em uma linguagem natural, a descrição do dispositivo pode ser muitas vezes ambígua, incompleta, ou até mesmo inconsistente. Além desses problemas, o device driver tem acesso a vários recursos do sistema operacional, assim qualquer erro nesta camada de software pode ser fatal. Por isso, essa camada de software deve ser cuidadosamente desenvolvida e testada. Com o intuito de reduzir os erros nos devices drivers, em MACIEIRA; BARROS; ASCENDINA (2014) foi proposta uma técnica de formalização e validação em tempo de execução de propriedades temporais e protocolos de comunicação de alto nível entre os dispositivos e seus devices drivers utilizando a linguagem TDevC. Mas, na especificação do trabalho anterior, a máquina de estados hierárquica gerada ainda pode conter estados não-determinísticos e propriedades temporais contraditórias. Dessa forma, o presente trabalho propõe uma técnica para validação de uma especificação TDevC para o desenvolvimento de device drivers robustos. Para isso, este trabalho faz uso do provador de teoremas de alto desempenho Z3 e das propriedades dos autômatos de Büchi. Para validação da proposta, foi utilizada a especificação TDevC do dispositivo Ethernet DM9000A.Nos experimentos realizados, verificou-se que o projeto conseguiu detectar as inconsistências na especificação TDevC em 100% dos casos.