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
- Lógicas para especificação formal
- Lógica proposicional (PL)
- Lógica de primeira ordem (FOL)
- Lógica relacional (RL)
- Lógica temporal linear (LTL)
- Técnicas de prova automática
- SAT solving para lógica proposicional
- SMT solving para lógica e teorias de primeira ordem
- Model-finding via SAT para lógica relacional
- Bounded model-checking via SAT para lógica temporal
- Conceção formal de software com Alloy
- Modelação estrutural
- Modelação comportamental
- Teste automático baseado em modelos
- Especificação e verificação de programas com Why3
- Linguagem lógica, teorias (biblioteca) e prova
- Linguagem de programas, especificação comportamental, e verificação de correção
- Desenvolvimento de sistemas com estado
Docentes
- Nuno Macedo (NM)
- Jorge Sousa Pinto (JSP)
- Maria João Frade (MJF)
Avaliação
- Época normal
- Exercícios de avaliação (20%)
- Teste individual (80%)
- Época de recurso
- Exame individual (100%)
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
- Logic in Computer Science: Modelling and Reasoning About Systems. Michael Huth & Mark Ryan. Cambridge University Press; 2nd edition (2004).
- The Calculus of Computation: Decision Procedures with Applications to Verification. Aaron R. Bradley & Zohar Manna. Springer (2007).
- Rigorous Software Development: An Introduction to Program Verification. J.B. Almeida & M.J. Frade & J.S. Pinto & S.M. de Sousa. Springer (2011).
- Software Abstractions: Logic, Language, and Analysis (revised edition). Daniel Jackson. MIT Press (2012).
- The Essence of Software: Why Concepts Matter for Great Design. Daniel Jackson. Princeton University Press (2021)
- Formal Software Design with Alloy 6. Julien Brunel, David Chemouil, Alcino Cunha, and Nuno Macedo (2021).
Outras leituras recomendadas
- D. Jackson. Alloy: a language and tool for exploring software designs. Commun. ACM 62(9): 66-76 (2019). Também existe um vídeo sobre este artigo que pode ser visto aqui.
- Leslie Lamport. If You’re Not Writing a Program, Don’t Use a Programming Language. Bulletin of the EATCS 125 (2018)
- David Benavides, Sergio Segura, Antonio Ruiz Cortés: Automated analysis of feature models 20 years later: A literature review. Inf. Syst. 35(6): 615-636 (2010)
Ferramentas
- SAT solvers
- SMT solvers (SMT-LIB - The Satisfiability Modulo Theories Library)
- Alloy
- Why3