Disciplina
Especificação de Software
Área
Área Científica de Metodologia e Tecnologias da Programação > Engenharia de Software
Activa nos planos curriculares
MEIC-T 2018 > MEIC-T 2018 > 2º Ciclo > Agrupamentos > Engenharia de Software > Especificação de Software
MEIC-T 2021 > MEIC-T 2021 > 2º Ciclo > Área Principal > Agrupamentos > Engenharia de Software > Especificação de Software
MEIC-T 2015 > MEIC-T 2015 > 2º Ciclo > Agrupamentos > Engenharia de Software > Especificação de Software
MEIC-A 2021 > MEIC-A 2021 > 2º Ciclo > Area Principal > Agrupamentos > Engenharia de Software > Especificação de Software
MEIC-A 2015 > MEIC-A 2015 > 2º Ciclo > Agrupamentos > Engenharia de Software > Especificação de Software
MEIC-T 2006 > MEIC-T 2006 > 2º Ciclo > Áreas de Especialização Complementares > Engenharia de Software > Especificação de Software
MEIC-A 2006 > MEIC-A 2006 > 2º Ciclo > Área de Especialização Complementar > Engenharia de Software > Especificação de Software
Nível
Método de Avaliação: 2 Projectos + 2 Testes
Tipo
Não Estruturante
Regime
Semestral
Carga Horária
1º Semestre
3.0 h/semana
1.5 h/semana
147.0 h/semestre
Objectivos
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.
Metodologia de avaliação
Método de Avaliação: 2 Projectos + 2 Testes
Pré-requisitos
Componente Laboratorial
Princípios Éticos
Componente de Programação e Computação
Componente de Competências Transversais
Bibliografia
Principal
Modeling in Event-B - System and Software Engineering
Cambridge University Press - ISBN 978-0-521-89556-9
Software Abstractions, Logic, Language, and Analysis
The Calculus of Computation: Decision Procedures with Applications to Verification
Aaron R. Bradley and Zohar Manna