Disciplina Curricular
Especificação de Software QS
Mestrado Bolonha em Engenharia Informática e de Computadores - Taguspark - MEIC-T 2021
Contextos
Grupo: MEIC-T 2021 > 2º Ciclo > Área Principal > Agrupamentos > Engenharia de Software
Período:
Peso
6.0 (para cálculo da média)
Pré-requisitos
Esta UC requere familiaridade com programação imperativa e orientada por objectos bem como noções elementares de matemática discreta.
Objectivos
Conhecer especificações formais e métodos formais para a engenharia de software, assim como as ferramentas/métodos de análise automática das propriedades dos programas. A disciplina fornece conhecimentos em: 1. Desenho e modelação de sistemas de software usando uma linguagem de especificação formal. Verificação automática de modelos e das suas propriedades. Linguagem de especificação declarativa para expressar restrições e comportamento de sistemas de software. Estados e traços. Modelação estática e dinâmica. 2. Verificação automática de programas (funcionais e imperativos) contra especificações. Verificação de propriedades funcionais. Construção de programas verificados através da anotação de código com teoremas, pré- e pós-condições, invariantes de ciclo, asserções, etc.
Programa
Introdução - Motivação para a utilização de especificações e métodos formais; Verificação de modelos vs procura de modelos vs prova de teoremas; Motivação para o uso de ferramentas de métodos formais; Linguagens declarativas vs operacionais. O Analisador Alloy - Introdução: Vantagens das abstrações; Sintaxe. Lógica no Alloy: Combinação de quantificadores de FOL com operadores de cálculo relacional; Átomos e relações. Linguagem: factos, asserções, predicados, funções. Verificação de modelos e as suas propriedades. Modelação estática e dinâmica. A linguagem Dafny - Introdução: Anotações e construção de programas verificados. Linguagem: Classes genéricas, afetação dinâmica, tipos de dados indutivos; Construções da especificação: pré- e pós-condições, invariantes de ciclo, asserções, especificações de enquadramento. Construções fantasma. Tipos coleção. Verificação de anotações e desenvolvimento de provas. Desenvolvimento incremental de programas imperativos verificados.
Metodologia de avaliação
Exame (50%) e dois projectos (25% + 25%)
Componente de Competências Transversais
Explicitar as Competências Transversais a desenvolver de acordo com o definido pela comissão de competências transversais, indicando qual a percentagem das suas componentes de avaliação que contempla a análise de competências transversais.
Componente Laboratorial
Exercícios em FOL, escrita de especificações usando o Analisador Alloy, lógica de Hoare, construção de programas verificados usando Dafny. Apoio ao projeto.
Componente de Programação e Computação
No curso onde esta UC é oferecida estão asseguradas as componentes de Computação e Programação de acordo com o MEPP 2122.
Princípios Éticos
Todos os membros de um grupo são responsáveis pelo trabalho do grupo. Em qualquer avaliação, todo aluno deve divulgar honestamente qualquer ajuda recebida e fontes usadas. Numa avaliação oral, todo aluno deverá ser capaz de apresentar e responder a perguntas sobre toda a avaliação.