Banca de QUALIFICAÇÃO: SAMUEL LINCOLN MAGALHAES BARROCAS
Uma banca de QUALIFICAÇÃO de DOUTORADO foi cadastrada pelo programa.
DISCENTE : SAMUEL LINCOLN MAGALHAES BARROCAS
DATA : 14/02/2017
HORA: 09:00
LOCAL: IMD - CIVT B321
TÍTULO:
Uma Estratégia para Validar o Gerador de Códigos de Circus para Java
PALAVRAS-CHAVES:
Métodos Formais, verificação de código, validação, Circus
PÁGINAS: 100
RESUMO:
Métodos Formais são técnicas usadas para prevenir erros no desenvolvimento de Sistemas de Software. Como o processo de desenvolver Software a partir de Métodos Formais é laborioso e propenso a erros, Geradores Formais de Código são usados. O uso dessas ferramentas reduz chances de erros na implementação de Sistemas de Software a partir de especificações formais. Como também pode haver erros no processo de geração de Software a partir da especificação de entrada, um esforço interessante é provar que o código gerado corretamente implementa a especificação de entrada. Esta Proposta de Doutorado visa elaborar uma estratégia baseada em cobertura e verificação de código para validar JCircus, um tradutor de especificações em Circus concretas para código Java. Esta estratégia de validação engloba a implementação de um Gerador de Sistemas de Transições Rotuladas (LPTSGen) para Circus (baseado em uma Semântica Operacional Estrutural para Circus ) e a sua conversão para JPF (Java Pathfinder), um verificador de modelos em Java. Visando atingir este objetivo, o modelo em JPF deve conduzir o código gerado por JCircus.
Esta Proposta de Doutorado também mostra resultados parciais na prova de solidez das regras da Semântica Operacional Estrutural com respeito às Teorias Unificadas de Programação (UTP). O papel da prova de solidez é fortalecer a validação
MEMBROS DA BANCA:
Presidente - 1639701 - MARCEL VINICIUS MEDEIROS OLIVEIRA
Interno - 1221251 - MARTIN ALEJANDRO MUSICANTE
Interno - 1709820 - ROBERTA DE SOUZA COELHO