Métodos Formais em Engenharia de Software

Mestrado em Engenharia Informática

2021/22

AVISO: Tendo havido e-mails de alunos impossibilitados de vir ao teste por estarem em isolamento, transcreve-se o disposto no Despacho RT-04/2022, de 13-Janeiro, sobre essa situação:

  1. Os estudantes que não possam comparecer presencialmente às avaliações das unidades curriculares na época normal, por se encontrarem em isolamento, devido a infeção por SARS-CoV2, ou em situação de isolamento profilático decretado pela autoridade de saúde competente, podem, mediante apresentação da devida declaração, realizar a avaliação na época de recurso;
  2. Os estudantes que não possam comparecer presencialmente nas avaliações na época de recurso, por se encontrarem em isolamento, devido a infeção por SARS-CoV2, ou em situação de isolamento profilático decretado pela autoridade de saúde competente, podem, mediante apresentação da devida declaração, realizar a avaliação numa época excecional que decorrerá no período de 14 a 19 de fevereiro de 2022;

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 trabalhos de casa serão propostos no final de algumas aulas teóricas e serão para submeter na plataforma de e-learning dentro do prazo limite definido.

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
Teórica   2ª 08h-10h CP1 0.08
Teórico-prática 1 2ª 11h-12h CP1 2.05
Teórico-prática 2 2ª 14h-15h CP1 1.25
Teórico-prática 3 5ª 16h-17h CP1 2.25
Teórico-prática 4 3ª 11h-12h CP1 1.15

Planificação

# Data Docentes Sumário
1 4 Out JNO, MAC Introdução aos Métodos Formais. Apresentação da UC.
2 11 Out MJF Lógica proposicional. SAT solving.
3 18 Out MJF Lógica de 1ª ordem. Modelação em FOL.
4 25 Out MJF Teorias de 1ª ordem. SMT solvers.
5 8 Nov MAC Modelação estrutural com Alloy.
6 15 Nov MAC Modelação estrutural com Alloy. Tópicos avançados sobre Alloy.
7 22 Nov MAC Tópicos avançados sobre Alloy. Modelação comportamental com Alloy.
8 29 Nov MAC Modelação comportamental com Alloy.
9 6 Dez JSP Especificação e verificação dedutiva de programas C: segurança de execução.
10 13 Dez JSP Especificação e verificação dedutiva de programas C: propriedades funcionais.
11 3 Jan JSP Especificação e verificação dinâmica de programas C.
12 10 Jan LSB, RN Introdução aos métodos formais para sistemas ciber-físicos.
  14 Jan MAC, MJF, JSP Teste.
  4 Fev MAC, MJF, JSP Exame.

Trabalhos de casa

Material

Slides

Exercícios

Exemplos

Testes

Bibliografia

Outras leituras recomendadas

Ferramentas