PPgSC/UFRN PROGRAMA DE PÓS-GRADUAÇÃO EM SISTEMAS E COMPUTAÇÃO ADMINISTRAÇÃO DO CCET Téléphone/Extension: (84)3342-2225/115 https://posgraduacao.ufrn.br/ppgsc

Banca de DEFESA: SAMUEL LINCOLN MAGALHAES BARROCAS

Uma banca de DEFESA de DOUTORADO foi cadastrada pelo programa.
DISCENTE : SAMUEL LINCOLN MAGALHAES BARROCAS
DATA : 22/02/2018
HORA: 14:00
LOCAL: IMD/CIVT - B321
TÍTULO:

Uma Estratégia para Validar a Geração de Códigos de Circus para Java


PALAVRAS-CHAVES:

Métodos Formais, Verificação de modelos, Testes de Software, Síntese de Código, Circus


PÁGINAS: 100
RESUMO:

O uso de Geradores Automáticos de Código para Métodos Formais não apenas minimiza esforços na implementação de Sistemas de Software, como também reduz a chance da existência de erros na execução destes Sistemas. Estas ferramentas, no entanto, podem ter faltas em seus códigos-fontes que causam erros na geração dos Sistemas de Software, e então a verificação de tais ferramentas é encorajada. Esta tese de Doutorado visa criar e desenvolver uma estratégia para verificar JCircus, um Gerador Automático de Código de um amplo sub-conjunto de Circus para Java. O interesse em Circus vem do fato de que ele permite a especificação dos aspectos concorrentes e de estado de um Sistema de maneira direta. A estratégia de verificação consiste nos seguintes passos: (1) extensão da Semântica Operacional de Circus existente e prova de que ela é sólida com respeito à Semântica Denotacional existente de Circus na Teoria Unificada de Programação (UTP), que é um framework que permite prova e unificação entre diferentes teorias; (2) desenvolvimento e implementação de uma estratégia que verifica o refinamento do código gerado por JCircus, através de uma toolchain que engloba um Gerador de Sistema de Transições Rotuladas com Predicado (LPTS) para Circus e um Gerador de Modelos que aceita como entrada o LPTS e gera um Oráculo que usa o verificador de modelos Java Pathfinder, que checa o refinamento do código gerado por JCircus. Combinado com técnicas baseadas em cobertura de código, nós visamos aumentar a confiabilidade do código gerado de Circus para Java.


MEMBROS DA BANCA:
Presidente - 1639701 - MARCEL VINICIUS MEDEIROS OLIVEIRA
Interno - 1221251 - MARTIN ALEJANDRO MUSICANTE
Interno - 1495704 - UMBERTO SOUZA DA COSTA
Externo à Instituição - ALEXANDRE CABRAL MOTA - UFPE
Externo à Instituição - BRUNO EMERSON GURGEL GOMES - IFRN
Notícia cadastrada em: 02/01/2018 20:03
SIGAA | Superintendência de Tecnologia da Informação - (84) 3342 2210 | Copyright © 2006-2024 - UFRN - sigaa07-producao.info.ufrn.br.sigaa07-producao