Formal Methods in Software Engineering — Métodos Formais em Engenharia de Software

Master in Informatics Engineering — Mestrado em Engenharia Informática

2023/24

Esta unidade curricular do 1º semestre do 1º ano do Mestrado em Engenharia Informática da Universidade do Minho tem por objectivo 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 avaliação contínua quer no exame) terão que ser defendidas através da realização de um pequeno projecto.

Horário

Tipo Turno Horário Sala Docente
Teórica   2ª 9h-11h CP2 0.01  
Teórico-prática 1 2ª 15h-16h CP2 2.04 JSP
Teórico-prática 2 2ª 12h-13h CP1 2.20 JSP
Teórico-prática 3 2ª 12h-13h CP1 1.25 MAC
Teórico-prática 4 2ª 15h-16h CP1 2.14 MAC
Teórico-prática 5 2ª 12h-13h CP1 1.17 MJF

Planificação

# Data Docentes Sumário
1 11 Set   Apresentação da UC.
2 18 Set MJF Lógica proposicional. SAT solvers. Modelação em PL.
3 25 Set MJF Lógica de 1ª ordem. Modelação em FOL.
4 2 Out MJF Teorias de 1ª ordem. SMT solvers. Modelação em FOL com teorias de 1ª ordem.
  6 Out   Entrega do 1º exercício de avaliação.
5 9 Out MJF Formalização de modelos de domínio em FOL.
6 16 Out MAC Introdução à modelação estrutural em Alloy: assinaturas e relações, lógica relacional. Formalização de modelos de domínio em Alloy e RL.
7 23 Out MAC Modelação estrutural em Alloy: relações de aridade superior, técnicas de validação, sistema de tipos, model finding para RL.
  27 Out   Entrega do 2º exercício de avaliação.
8 30 Out MAC Introdução à modelação comportamental com Alloy: especificação de sistemas com estado, técnicas de validação.
9 6 Nov MAC Modelação comportamental com Alloy: lógica temporal linear, especificação e verificação de requisitos comportamentais em LTL, bounded model-checking para LTL.
  10 Nov   Entrega do 3º exercício de avaliação.
10 13 No JSP Introdução ao Why3. Linguagem lógica e verificação de programas funcionais.
11 20 Nov JSP Verificação de programas imperativos com Why3. Desenvolvimento de módulos com estado.
12 27 Nov JSP Desenvolvimento e verificação de “software concepts” em Why3: implementação baseada em conjuntos.
13 4 Dez JSP Desenvolvimento e verificação de “software concepts” em Why3: implementação eficiente.
  8 Dec   Entrega do 4º exercício de avaliação.
  16 Dec   TESTE ( 9h00, salas: Edificio 2 - 0.01+1.05+1.07+2.02 )
  20 Jan   EXAME

Exercícios de avaliação

# Tópico Deadline
1 Modelação em PL e FOL. 6 Out
2 Modelação estrutural em Alloy. 27 Out
3 Modelação comportamental em Alloy. 10 Nov
4 Desenvolvimento e verificação de sistemas com estado em Why3. 8 Dez

Material

Slides

Exercícios

Exemplos

Testes

Bibliografia

Outras leituras recomendadas

Ferramentas

Edições anteriores