Events Events

Back

Tese aborda contratos para a validação da comunicação de alto nível entre software e hardware

A apresentação ocorrerá na próxima segunda-feira (5), às 7h no auditório do Centro de Informática (CIn)

O Programa de Pós-Graduação em Ciência da Computação da UFPE promoverá a defesa da tese de doutorado “Técnica baseada em Contratos para a Validação da Comunicação de alto nível entre Software e Hardware”, de autoria do aluno Rafael Melo Macieira e orientada pela professora Edna Natividade da Silva Barros. 

O apresentação ocorrerá na próxima segunda-feira (5), às 7h no auditório do Centro de Informática (CIn). Na banca examinadora estarão presentes os professores André Luis de Medeiros Santos (CIn/UFPE), Alexandre Cabral Mota (CIn/UFPE), Victor Wanderley Costa de Medeiros (DeInfo/ UFRPE), Djones Vinicius Lettnin (Departamento de Engenharia Eletrônica/UFSC) e Fabian Luis Vargas (Departamento de Engenharia Elétrica/PUC-RS)

Resumo:

O uso de sistemas eletrônico embarcados em um amplo espectro de aplicações aumentou substancialmente. Telefones celulares, computadores de bordo, dispositivos IoT e sistemas cyberfísicos são alguns exemplos em que sistemas embarcados exigem mais flexibilidade para o processamento de diferentes tipos de aplicações e protocolos de comunicação. A necessidade desta flexibilidade elevada requer o uso de processadores de propósito geral como uma solução para configurar e controlar uma quantidade crescente de periféricos. No entanto, isso também implica uma necessidade crescente do uso de software dependente de hardware (HdS). Uma vez que HdS é um componente altamente crítico e propenso a erros devido à natureza do ambiente no qual está inserido e a sua difícil codificação, é importante que as fases de desenvolvimento e de operação destes componentes sejam suportadas por metodologias que tornem mais explícitas as violações de acessos aos periféricos através do acompanhamento de contratos definidos com base na especificação dos protocolos de comunicação. Assim, esta abordagem propõe uma técnica de formalização e validação em tempo de execução de propriedades temporais de protocolos de comunicação de alto nível entre os dispositivos e seus device drivers, comumente especificados baseados em uma documentação informal (datasheets), durante a simulação de plataformas virtuais ou execução de plataformas de hardware real. Para tornar essa técnica viável juntamente com metodologias consolidadas, uma linguagem específica foi desenvolvida para suportar a sua utilização como uma melhoria de modelos baseados na plataforma, permitindo um refinamento iterativo do protocolo de comunicação e das especificações das propriedades temporais juntamente com o refinamento da plataforma. Alguns experimentos usando um dispositivo DM9000A Ethernet e uma Altera UART mostrou que esta abordagem é eficaz na detecção de falha crítica indesejada em HdS, consumindo pouco tempo de projeto e impactando pouco ou, para plataformas de hardware real, nada no tempo de execução.

Date of last modification: 05/03/2018, 13:56