English

CIn - Centro de Informática UFPE




Eventos Relacionados

Defesa de Dissertação de Mestrado N° 1669 "Validação de uma Especificação TDevC para o Desenvolvimento de Device Drivers Robustos"

A aluna Vanessa Larize Alves de Carvalho irá defender sua pesquisa no dia 15 de setembro, às 8h30, na sala D220 do CIn-UFPE Início: 15/09/2016 às 08:30 Término: 15/09/2016 às 00:00 Local: Sala D220

Pós-Graduação em Ciência da Computação – UFPE

Defesa de Dissertação de Mestrado Nº 1.669

 

Aluna: Vanessa Larize Alves de Carvalho

Orientadora: Profa. Edna Natividade da Silva Barros

Título: Validação de uma Especificação TDevC para o Desenvolvimento de Device Drivers Robustos

Data: 15/09/2016

Hora/Local: 8h:30m – Centro de Informática – Sala D220

Banca Examinadora:

Profa. Edna Natividade da Silva Barros (CIn/UFPE)

Prof. André Aziz Camilo de Araujo  (DEINFO/UFRPE)

Prof. Giovanny Fernando Lucero Palma  (DCCE/UFS)

 

 

RESUMO:

 

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 as 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 ao projeto de software embarcado. Porém, devido a atual complexidade dos dispositivos, projetos de hardware não conseguem acompanhar o crescimento da capacidade do hardware, havendo um gap de produtividade entre o desenvolvimento do hardware e 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 destes problemas, o device driver tem acesso à 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, 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 ter estados não-determinísticos e propriedades temporais contraditórias. Desta 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 isto, este trabalho faz uso do provador de teoremas de alto desempenho Z3 e das propriedades dos autômatos de Büchi. Para validação do projeto, foi utilizada a especificação de um dispositivo Ethernet DM9000A.

Nos experimentos realizados verificou-se que o projeto conseguiu detectar as inconsistências na especificação TDevC em 100% dos casos.

 

 

PALAVRAS-CHAVE: Device Drivers, Validação de uma especificação TDevC, Provadores automáticos de teoremas, Autômatos de Buchi.

  • © Centro de Informática UFPE - Todos os direitos reservados
    Tel +55 81 2126.8430 - Cidade Universitária - 50740-560 - Recife/PE
Plano4 Consultoria Web