MFP
Índice
| Métodos Formais em Engenharia de Software |
|---|
| Cálculo de Sistemas de Informação |
| Programação Ciber-física |
| Verificação Formal |
| Calendário | Sumários |
| Anos anteriores |
| Alumni |
Verificação Formal
2023/24
Em UCs passadas, nomeadamente em MFES, já foi abordada a verificação dedutiva de algoritmos imperativos sequenciais e de algoritmos funcionais. Nesta UC serão abordadas técnicas para especificação e verificação de algoritmos não sequenciais, nomeadamente algoritmos concorrentes, self-stabilizing e distribuídos.
Na primeira parte será abordada a especificação de algoritmos usando TLA+, uma linguagem introduzida por Leslie Lamport precisamente com o objectivo de simplificar a especificação de algoritmos não sequenciais. As especificações em TLA+ podem ser verificadas automaticamente com o model-checker TLC, e esta abordagem lightweight fez com que o TLA+/TLC tenha sido frequentement adoptado pela indústria (e.g. Amazon) para verificar algoritmos complexos.
Na segunda parte será abordada a verificação dedutiva destes mesmos algoritmos, técnica que permitirá verificar a sua correção para qualquer configuração possível, o que não é possível com o model-checking que apenas pode ser usado para verificar um conjunto de configurações limitado. Para tal será usado o Why3, já previamente introduzido em MFES, uma ferramenta que usa SMT solvers para efectuar a prova automática das condições de verificação inerentes à verificação dedutiva.
Devido à indecidibilidade da lógica de primeira ordem (que está na base de qualquer especificação em TLA+ ou Why3), nem sempre será possível a prova automática das condições de verificação. Por isso, na última parte da UC serão abordadas técnicas de prova assisitida dessas mesmas condições, nomeadamente recorrendo à ferramenta de prova assistida Coq.
Programa
- Especificação e verificação de algoritmos não sequenciais (concorrentes, self-stablizing e distribuídos)
- Model-checking com TLA+/TLC
- Verificação dedutiva com Why3
- Prova assistida de condições de verificação com Coq
Docentes
- Alcino Cunha (MAC)
- Jorge Sousa Pinto (JSP)
- Maria João Frade (MJF)
Avaliação
- Avaliação contínua com duas provas de avaliação:
- Teste individual escrito sobre especificação e verificação de algoritmos não sequenciais (70%)
- Teste individual prático sobre prova assistida de condições de verificação (30%)
- O exame de recurso terá duas partes com as mesmas cotações
- 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 | Horário | Sala |
|---|---|---|
| Teórica | 6ªf. 9h-11h | Ed.7 0.09 |
| Teórico-prática | 6ªf. 11h-12h | Ed.7 0.09 |
Planificação
| # | Data | Docentes | Sumário |
|---|---|---|---|
| 1 | 9 Fev | MAC | Overview da linguagem TLA+ e do model-checker TLC. |
| 2 | 16 Fev | MAC | Especificação e verificação de algoritmos concorrentes com TLA+/TLC. |
| 3 | 23 Fev | MAC | Especificação e verificação de algoritmos self-stabilizing com TLA+/TLC. |
| 4 | 1 Mar | MAC | Especificação e verificação de algoritmos distribuídos com TLA+/TLC. |
| 5 | 8 Mar | JSP | Deductive Verification of Transition Systems in Why3. |
| 6 | 15 Mar | JSP | Verification of Concurrent Programs with Why3. |
| 7 | 22 Mar | JSP | Verification of Token-based Mutual Exclusion with Why3. |
| 8 | 5 Abr | JSP | Deductive Verification of Distributed Algorithms with Why3. |
| 9 | 12 Abr | MAC+JSP | 1º Teste |
| 10 | 19 Abr | MJF | Introdução ao Assistente de Prova Coq. |
| 11 | 26 Abr | MJF | Raciocínio Indutivo no Sistema Coq. |
| 12 | 3 Mai | MJF | Verificação de Algoritmos Funcionais em Coq. |
| 13 | 10 Mai | MJF | Coq |
| 15 Mai | MJF | 2º Teste | |
| 5 Jun | MAC+JSP+MJF | Exame |
Material
Exercícios
Exemplos
Bibliografia
- Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Leslie Lamport. Addison-Wesley, 2002.
- The TLA+ Video Course. Leslie Lamport. 2021.
- The Why3 Platform François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich. Version 1.4, March 2021
- The Coq Proof Assistant
Outras leituras recomendadas
- Shankar, A. U.: An introduction to assertional reasoning for concurrent systems. ACM Computing Surveys (CSUR), 25(3), 225-262, 1993.
- Leslie Lamport. If You’re Not Writing a Program, Don’t Use a Programming Language. Bulletin of EATCS, 125, June 2018.
- Yves Bertot. Coq in a Hurry. INRIA 2017.