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:
- 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;
- 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
- Lógicas para especificação formal
- Lógica proposicional
- Lógica de primeira ordem
- Lógica relacional
- Lógica temporal
- 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
- Concepção formal de software com Alloy
- Modelação estrutural
- Modelação comportamental
- Especificação e Verificação de Programas da Linguagem C
- Especificação comportamental: a linguagem ACSL
- Propriedades de segurança de execução e propriedades funcionais
- Especificação com base em contratos
- Verificação dedutiva de programas: condições de verificação para programas com contratos
- Verificação dinâmica de programas: monitorização
- Introdução à ferramenta Frama-C
- Utilização do IDE
- geração automática de anotações de segurança de execução com o plug-in RTE
- verificação dedutiva: o plug-in WP
- verificação dinâmica: o plug-in E-ACSL
- Especificação comportamental: a linguagem ACSL
- Introdução aos métodos formais para sistemas ciber-físicos
Docentes
- José Nuno Oliveira (JNO)
- Maria João Frade (MJF)
- Alcino Cunha (MAC)
- Jorge Sousa Pinto (JSP)
- Luís Soares Barbosa (LSB)
- Renato Neves (RN)
Avaliação
- Trabalhos de casa (25%)
- Teste individual (75%)
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
- SAT solving (entrega até 24 de Outubro, via Blackboard)
- SMT solving (entrega até 7 de Novembro, via Blackboard)
- Modelação estrutural com Alloy (entrega até 21 de Novembro, via Blackboard)
- Modelação comportamental com Alloy: circuitos Eulerianos (entrega até 8 de Dezembro, via Blackboard)
- Verificação do Algoritmo de Warshall (entrega até 14 de Janeiro, via Blackboard)
Material
Slides
- Propositional Logic & SAT Solvers
- First-Order Logic
- First-Order Theories & SMT Solvers
- Structural design with Alloy
- Mastering Alloy
- Protocol design with Alloy
- Verification of Software Safety Properties — An Introduction
- Safety Verification with Frama-C/WP
- Functional Verification with Frama-C/WP
Exercícios
- SAT solving
- Ficheiros DIMACS CNF
- Colab notebooks: PysatExemplo, Meeting, GraphColoring
- Formalização (de modelos de domínio) em FOL
- SMT solving
- Ficheiros SMT-LIB 2
- Colab notebooks: Z3Python, Suduko, Skyscrapers
- Alloy4Fun
- Alloy Analyzer
- Código C / ACSL
Exemplos
- CBMC: CBMC by example, ficheiros para teste
- Alloy: File system, Leader election
- Frama-C: remove_copy (example from the ACSL by Example text linked below – this folder is made availabe here for convenience, but you can always clone the full repo instead)
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. Daniel Jackson. MIT Press; revised edition (2012).
- 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)
Ferramentas
- SAT solvers
- SMT solvers
- Alloy
- Frama-C - Software Analyzers (disponível no Opam)