Banca de DEFESA: MADIEL DE SOUSA CONSERVA FILHO

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.

DISCENTE: MADIEL DE SOUSA CONSERVA FILHO

DATA: 07/10/2011

HORA: 09:00

LOCAL: sala de reuniões DIMAp

TÍTULO:

Estendendo CRefine para o Suporte de Táticas de Refinamento

PALAVRAS-CHAVES:

Métodos Formais, Circus, Táticas de Refinamento, ferramenta

PÁGINAS: 76

GRANDE ÁREA: Ciências Exatas e da Terra

ÁREA: Ciência da Computação

RESUMO:

Devido à necessidade da utilização de aplicações de software cada vez mais complexas, existe uma grande preocupação no que diz respeito em garantir uma melhor qualidade no processo de desenvolvimento de software. Assim, tanto profissionais quanto pesquisadores estão utilizando novas técnicas em conjunto com as já existentes na área de Engenharia de Software para tornar o desenvolvimento dos sistemas cada vez mais correto. Uma dessas abordagens são os Métodos formais, que utilizam linguagens formais que têm sua base fundamentada na matemática, apresentando uma semântica e  sintaxe bem definidas. Uma destas linguagens é Circus, a qual possibilita a modelagem de sistemas concorrentes. Ela foi desenvolvida com a união dos conceitos de outras duas linguagens de especificação, Z, que especifica a modelagem de dados complexos, com CSP, para a modelagem de sistemas concorrentes. Circus também possibilita realizar o processo de cálculo de refinamentos de programas, na qual leis de refinamento são aplicadas à uma especificação formal. A ferramenta CRefine foi desenvolvida para realizar o suporte a este cálculo de refinamentos de  programas em Circus.

Cada etapa é justificada pela aplicação de uma lei de refinamento  (possivelmente com o prova de certas condições chamadas de obrigações de prova). Às vezes, as mesmas leis podem ser aplicadas da mesma forma em diferentes desdobramentos ou mesmo em partes diferentes de um único desenvolvimento. Uma estratégia para otimizar esse cálculo é formalizar estas aplicações como táticas de refinamento, que podem ser usadas como uma regra única de transformação. 

Antes desta dissertação, CRefine não fornecia suporte para as táticas de refinamento. Este trabalho apresenta um novo módulo no CRefine, que automatiza o processo de definição e aplicação de táticas de refinamento que são formalizadas na linguagem tática ArcAngelC. Além  disso, validamos a extensão aplicando o novo módulo em um estudo de caso, que consiste em uma estratégia de refinamento para verificação de implementações SPARK Ada de sistemas de controle.

MEMBROS DA BANCA:
Interno - 1258224 - ANAMARIA MARTINS MOREIRA
Externo à Instituição - AUGUSTO CEZAR ALVES SAMPAIO - UFPE
Presidente - 1639701 - MARCEL VINICIUS MEDEIROS OLIVEIRA