Métodos Formais em Engenharia de Software

Mestrado em Engenharia Informática

2025/26

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   4ª 9h-10h ED1 0.08  
Teórico-prática 1 4ª 11h-13h ED2 0.01 JSP
Teórico-prática 2 4ª 11h-13h ED3 0.06 MJF
Teórico-prática 3 4ª 11h-13h ED1 2.26 NM

Planificação

# Data Docentes Sumário
1 24 Set NM Apresentação da UC. Lógica proposicional.
2 1 Out NM Lógica de 1ª ordem. Formalização de modelos de domínio em lógica de primeira ordem.
3 8 Out NM SAT solving e SMT solving .
  12 Out   Entrega do 1º exercício de avaliação.
4 15 Out NM Modelação estrutural em Alloy: declaração assinaturas e relações. Formalização de instâncias. Formalização de modelos de domínio em Alloy.
5 22 Out NM Modelação estrutural em Alloy: restrições estruturais, lógica de primeira ordem e relacional, predicados e funções.
6 29 Out NM Tópicos avançados sobre modelação estrutural em Alloy: relações de aridade superior, overloading, sistema de tipos. Teste automática baseado em modelos.
  2 Nov   Entrega do 2º exercício de avaliação.
7 5 Nov NM Modelação comportamental com Alloy: especificação e validação de sistemas de transição de estado usando lógica temporal. Software concept design com Alloy.
8 12 Nov NM Modelação comportamental com Alloy: especificação e verificação de requisitos em lógica temporal. App design com Alloy.
  16 Nov   Entrega do 3º exercício de avaliação.
9 19 Nov JSP Verificação de programas funcionais com Why3.
10 26 No JSP Desenvolvimento de módulos com estado em Why3. Verificação de invariantes.
11 3 Dez JSP Especificação e verificação de “software concepts” em Why3. Implementação funcional.
12 10 Dez JSP Refinamento de módulos em Why3 e extração de código WhyML correcto. Implementação imperativa de “software concepts”.
13 17 Dez   (apenas aulas TP)
  21 Dez   Entrega do 4º exercício de avaliação.
      TESTE
      EXAME

Exercícios de avaliação

# Tópico Deadline
1 Modelação em PL. 12 Out
2 Modelação estrutural em Alloy. 2 Nov
3 Modelação comportamental em Alloy. 116 Nov
4 Desenvolvimento e verificação de sistemas com estado em Why3. 21 Dez

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