Defesa de Qualificação: Allberson Bruno de Oliveira Dantas

Título: Componentes Certificadores em uma Plataforma de Nuvem Computacional para Serviços de Computação de Alto Desempenho.

Data: 28/04/2016 Horário: 10h Local: Sala de Seminários do Bloco 952

Resumo:

O desenvolvimento de aplicações de Computação de Alto Desempenho (CAD) corretas e seguras é um desafio para desenvolvedores, uma vez que tais aplicações utilizam paralelismo e estão inseridas em ambientes de programação heterogêneos. Esta proposta de Tese de Doutorado apresenta uma arquitetura que permite a construção de componentes certificados, os quais podem ser utilizados para compor aplicações de CAD em uma nuvem de componentes chamada HPC Shelf. Os componentes certificadores arquitetados nesse trabalho se dividem em duas espécies distintas: SWC2 e C4. Componentes SWC2 são utilizados para verificar propriedades formais sobre workflows na HPC Shelf. Já os componentes C4 são empregados para verificar propriedades formais em componentes de computação. Existe ainda a espécie TC, os quais representam na nuvem infraestruturas de verificação formal de software e podem ser orquestrados, mediante a linguagem TCOL, por certificadores a fim de potencializar a verificação das propriedades formais. Esperamos contribuir com o estado da arte nos seguintes pontos: em nuvens computacionais, fornecendo um serviço exclusivo para verificação formal de software; em plataformas orientadas a componentes, provendo componentes que podem verificar propriedades de outros de forma plug-and-play; possibilitando a orquestração automática de provadores para provar um conjunto de objetivos de prova; e em a aplicações de CAD, fornecendo um estudo sobre quais ferramentas de verificação formal de software se aplicam na verificação de suas propriedades.

Banca:

  • Prof. Dr. Francisco Heron de Carvalho Junior (MDCC/UFC - Orientador)
  • Prof. Dr. Luís Soares Barbosa (UMINHO - Portugal)
  • Prof. Dr. Pedro Porfírio Muniz Farias (UNIFOR)
  • Prof. Dr. Pablo Mayckon Silva Farias (UFC)