Métodos Formais em Engenharia de Software

Mestrado em Engenharia Informática

2024/25

Esta unidade curricular do 1º semestre do 1º ano do Mestrado em Engenharia Informática da Universidade do Minho tem por objetivo introduzir a utilização dos Métodos Formais na Engenharia de Software.

Os alunos interessados em aprofundar os conhecimentos adquiridos nesta unidade curricular podem optar por frequentar o perfil de Métodos Formais de Programação no 2º semestre.

Programa

Docentes

Avaliação

Os exercícios de avaliação serão propostos no final de algumas aulas teóricas e serão para submeter na plataforma de e-learning na 6ª feira seguinte.

As notas acima de 18 valores (quer na época normal, quer na época de recurso) terão que ser defendidas através da realização de um pequeno projeto / desafio.

Horário

Tipo Turno Horário Sala Docente
Teórica   2ª 13h-15h CP1 0.08  
Teórico-prática 1 2ª 15h-16h CP2 2.02 JSP
Teórico-prática 2 2ª 11h-12h CP2 2.06 JSP
Teórico-prática 3 2ª 15h-16h ED7 1.10 MAC
Teórico-prática 4 2ª 11h-12h CP1 0.17 MAC
Teórico-prática 5 2ª 17h-18h CP1 2.23 MAC

Planificação

# Data Docentes Sumário
1 9 Set MAC Apresentação da UC. Lógica proposicional. Análise de modelos de variabilidade com lógica proposicional.
2 16 Set MAC SAT solving. Resolução de problemas de alocação com lógica proposicional.
3 23 Set MAC Lógica de 1ª ordem. Formalização de modelos de domínio em lógica de primeira ordem.
  27 Set   Entrega do 1º exercício de avaliação.
4 30 Set MAC Modelação estrutural em Alloy: declaração assinaturas e relações, lógica relacional. Formalização de modelos de domínio em Alloy.
5 7 Out MAC Tópicos avançados sobre modelação estrutural em Alloy: relações de aridade superior, overloading, predicados e funções, sistema de tipos. Teste automática baseado em modelos.
6 14 Out MAC Modelação comportamental com Alloy: especificação e validação de sistemas de transição de estado usando lógica temporal. Software concepts design com Alloy.
  18 Out   Entrega do 2º exercício de avaliação.
7 21 Out MAC Modelação comportamental com Alloy: especificação e verificação de requisitos em lógica temporal. App design com Alloy.
8 28 Out JSP Introdução ao Why3. Linguagem lógica. Modelos de domínio em Why3.
  1 Nov   Entrega do 3º exercício de avaliação.
9 4 Nov JSP Verificação de programas funcionais com Why3.
10 11 No JSP Desenvolvimento de módulos com estado em Why3. Verificação de invariantes.
11 18 Nov JSP Especificação e verificação de “software concepts” em Why3. Implementação funcional.
12 25 Nov JSP Verificação de programas imperativos com Why3. Implementação imperativa de “software concepts”.
  29 Nov   Entrega do 4º exercício de avaliação.
13 2 Dez    
  14 Dez   TESTE
  20 Jan   EXAME

Exercícios de avaliação

# Tópico Deadline
1 Modelação em PL. 27 Set
2 Modelação estrutural em Alloy. 18 Out
3 Modelação comportamental em Alloy. 1 Nov
4 Desenvolvimento e verificação de sistemas com estado em Why3. 29 Nov

Material

Slides das aulas teóricas

Exemplos das aulas teóricas

Exercícios das aulas teórico-práticas

Testes

Bibliografia

Outras leituras recomendadas

Ferramentas

Edições anteriores