Submitted by Alice Araujo (alice.caraujo@ufpe.br) on 2017-11-29T17:56:29Z No. of bitstreams: 2 license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5) dissertação_vanessa_larize_final.pdf: 1152292 bytes, checksum: 2bd44824bd4445f9e134fc21621a468a (MD5) / Made available in DSpace on 2017-11-29T17:56:29Z (GMT). No. of bitstreams: 2 license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5) dissertação_vanessa_larize_final.pdf: 1152292 bytes, checksum: 2bd44824bd4445f9e134fc21621a468a (MD5) Previous issue date: 2016-09-15 / FACEPE / 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. / The use of electronic embedded system has increased substantially. Mobile phones, Global Positioning System (GPS) and Digital television with LCD screens are examples of equipments that are incorporating features to meet the demands of users, and thereby increasing the complexity of embedded systems in these devices. In fact, the vast majority of innovations in embedded systems is attributed to advances in microelectronics and embedded software design. However, due to the current complexity of devices, hardware design cannot keep up the hardware capacity growth, with a productivity gap between the development of the hardware and the development of the software required for its operation. These softwares, also known as Hardware-dependent Software (HdS) are at the center of the design challenge systems. Among these HdS are the devices drivers. Drivers are encoded based on the documentation available by the hardware vendors, however, most of the time, this document is not easy to read and can lead to misinterpretations. Coupled to this, as this documentation is written in a natural language, the device description can often be ambiguous, incomplete or even inconsistent. In addition to these problems, the device driver has access to various operating system resources, so any error in this software layer can be fatal. Therefore, this software layer must be carefully developed and tested. In order to reduce errors in the device drivers, it has been proposed a technique for formalization and runtime validation of temporal properties in high-level communication protocols between devices and drivers using the TDevC language. But the hierarchical state machine, generate in the previous work, may contain nondeterministic states and contradictory temporal properties. Thus, this approach proposes a technique to validate a TDevC specification for the development of robust device drivers. Therefore, this work makes use of high-performance theorem prover Z3 and Buchi automata properties. Some experiments using the Ethernet device DM9000A TDevC specification showed that this approach is effective in detect TDevC specification inconsistency.