FenixEdu™

Aprender técnicas formais para especificação de requisitos e desenvolvimento de software. Entender a importância e aprender métodos para a verificação da correcção de programas. Utilização de ferramentas automáticas para verificação programas.

Programa

Especificação de Software usando Event-B - Especificação de Requisitos: Representação de Estados e de Invariantes. Construção de Modelos. - Event-B: Primitivas, Proof Obligations e Semântica Denotacional. - Refinamento de Requisitos como processo de desenvolvimento de software. - Correcção de Modelos e Refinamentos: Provas de correcção como método de verificação de software e de detecção de erros. - Modelação de Concorrência, Não Determinismo e Sistemas Distribuídos. - Desenvolvimento de programas imperativos. - Ferramentas Automáticas de Verificação: A plataforma Rodin. TOOLS: http://www.event-b.org/index.html Especificação de Software em Alloy - Diferenças entre Theorem Proving e Model-Checking. - Introdução ao Alloy: Sintaxe - Átomos, Relações e Restrições. - Semântica: Predicados e Restrições como forma de representar estados e execuções de programas. - Refinamento: Adição de restrições como processo de Refinamento. - Satisfação de Restrições e Predicados como processo de verificação. - Ferramentas Automáticas de Verificação: Alloy Analyzer. - Comparação com geração de casos de teste. TOOLS: http://alloy.mit.edu/alloy/ Verificação de Software - A linguagem pi: Sintaxe e Anotações. Pre e Pós-Condições. - Utilização de Substituições para definir o estado de um programa - Propriedades de Safety e Liveness. - Indução e funções de Ranking - Correcção de Ciclos e Recursão. - Estratégias para provar correcção de programas.