A prova de Mestrado em Engenharia Informática, requerida por Mário André Barbosa Eiras e subordinada ao tema "Formalizando Alloy com uma tradução para Isabelle/HOL", realiza-se no dia 14 de dezembro de 2011 pelas 16h00, no anfiteatro A2 do Departamento de Informática. A sessão é aberta a todos os interessados.
O júri para esta prova tem a seguinte composição:
- António Costa (UMinho) - presidente
- Simão de Sousa (UBI) - arguente
- Alcino Cunha (UMinho) - orientador
Resumo da dissertação
Métodos formais são técnicas desenvolvidas com uma base matemática cujo objetivo é garantir um elevado nível de qualidade num produto de software. Entre este conjunto de técnicas existem algumas que privilegiam a simplicidade de uso sobre a fiabilidade dos resultados, a fim de reduzir os recursos que estas abordagens exigem. Estes métodos formais conhecidos como "leves", enfatizam a especificação parcial e análise automática.
Alloy é uma linguagem de especificação declarativa criada para ser "leve". Ela foi criada juntamente com uma ferramenta de model checking designada por Alloy Analyzer que pode analisar automaticamente as especificações e procura contra exemplos num pequeno universo. Contudo, por vezes uma abordagem como model checking não é suficiente e a verificação total é necessária.
Neste trabalho definimos uma estratégia para incorporar a lógica do Alloy na lógica do theorem prover Isabelle/HOL e implementámos uma ferramenta para executar automaticamente essa tradução, permitindo a verificação de especificações em Alloy através do uso de um theorem prover.
21.11.2011
