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