Título: Certificação de Componentes em uma Plataforma de Nuvens Computacionais para Serviços de Computação de Alto Desempenho.

Data: 01/12/2016 Horário: 13h Local: Sala de Seminários do Bloco 952 - Campus do Pici

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 geralmente utilizam paralelismo e executam em plataformas heterogêneas de computação paralela. A Tese de Doutorado proposta neste documento dispõe-se a apresentar a arquitetura de um mecanismo de certificação de componentes para plataformas de nuvens computacionais de serviços de computação de alto desempenho. Em particular, esse mecanismo é proposto no contexto da plataforma HPC Shelf, permitindo a construção de componentes certificados quanto a propriedades funcionais e não funcionais, os quais podem ser utilizados para compor aplicações voltadas a usuários especialistas.Dois componentes certificadores são propostos utilizando o mecanismo de certificação introduzido na Tese: SWC2 (Scientific Workflow Certifier Component) e C4 (Computation Component Certifier Component). 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. Existem ainda os componentes táticos, os quais expõem os serviços de infraestruturas de verificação formal de software, os quais podem ser orquestrados, por certificadores, por meio da linguagem TCOL (Tactical Component Orchestration Language).Esperamos contribuir com o estado da arte nos seguintes pontos: em nuvens computacionais, fornecendo a primeira infraestrutura em nuvem voltada à verificação formal de software utilizando técnicas de computação de alto desempenho; em plataformas orientadas a componentes, provendo componentes não disruptivos que podem certificar outros de uma forma reflexiva; possibilitando a criação dos assim chamados sistemas de certificação paralela, os quais são formados por orquestrações de provadores para verificar propriedades formais; e em aplicações de computação de alto desempenho, 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)
• Prof. Dr. Lincoln de Souza Rocha (MDCC/UFC)
• Prof. Dr. Pablo Mayckon Silva Farias (UFC)
• Prof. Dr. Ricardo Massa Ferreira Lima (UFPE)