FenixEdu™

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

A avaliação da cadeira de Arquitecturas de Software é composta pelos seguintes elementos: Exame teórico: 40% da nota final, nota mínima de 8.5 valores (em 20) Mini testes: 40% da nota final, 4 mini testes realizadas durante as aulas práticas, são consideradas as 3 melhores notas Trabalhos práticos (em grupo): 20% da nota final A nota final é calculada de acordo com a fórmula NotaFinal = roundHalfUp(0.4 x E + 0.4 x MT + 0.2 x TP) em que "E", "MT" e "TP" correspondem às notas (de 0 a 20 valores) do Exame, Mini Testes e dos Trabalhos Práticos, respectivamente. A nota dos mini testes é calculada MT = ((MT1 + ... + MT4) - MIN(MT1, ... , MT4))/3. A nota dos trabalhos práticos "TP" é a média aritmética, sem arredondamentos, das notas obtidas em cada um dos trabalhos práticos realizados. Opção para trabalhadores estudantes: Os alunos que tiverem o estatuto de trabalhador-estudante realizam apenas exame final, cujo peso na nota final é de 100%. Em época especial será realizado um exame, cujo peso na nota final é de 100%.

Tipo

Não Estruturante

Regime

Semestral

Carga Horária

1º Semestre

Aula Teórica (T): 3.0 h/semana

Aula de Laboratório (PL): 1.5 h/semana

Trabalho Autónomo: 147.0 h/semestre

Créditos ECTS:

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; Métodos formais na indústria; Verificação de modelos vs procura de modelos vs prova de teoremas; Propriedades de segurança e de animação; Razões para usar ferramentas de métodos formais; Linguagens declarativas vs operacionais. O Analisador Alloy (http://alloy.mit.edu/alloy/): Introdução; Vantagens das abstrações; Sintaxe. Lógica no Alloy: Combinação de quantificadores de FOL com operadores de cálculo relacional; Estilo cálculo de predicado, estilo expressão de navegação, estilo 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: (https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/): 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.