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
2024/25
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.
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
Docentes
- Alcino Cunha (MAC)
- Jorge Sousa Pinto (JSP)
Avaliação
- Avaliação contínua com duas provas de avaliação:
- Teste individual escrito sobre model-checking (50%)
- Teste individual escrito sobre verificação dedutiva (50%)
- O exame de recurso terá duas partes com as mesmas cotações
- As notas iguais ou superiores a 19 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 | 4ªf. 9h-11h | CP2 2.11 |
| Teórico-prática | 4ªf. 11h-12h | CP2 2.11 |
Planificação
| # | Data | Docentes | Sumário |
|---|---|---|---|
| 1 | 5 Fev | MAC | Introdução ao TLA+: a Temporal Logic of Actions, especificação de sistemas de transição de estados, propriedades de safety. |
| 2 | 12 Fev | MAC | Introdução ao TLA+: propriedades de liveness e refinamento. Especificação e verificação de algoritmos concorrentes com TLA+. |
| 3 | 19 Fev | MAC | Especificação e verificação de algoritmos concorrentes com TLA+. |
| 4 | 26 Fev | MAC | Especificação e verificação de algoritmos self-stabilizing com TLA+. |
| 5 | 5 Mar | MAC | Especificação e verificação de algoritmos distribuídos com TLA+. |
| 6 | 12 Mar | MAC | Especificação e verificação de algoritmos distribuídos com TLA+. |
| 7 | 19 Mar | MAC | 1º Teste |
| 8 | 26 Mar | JSP | Verificação dedutiva de sistemas de transição em Why3 |
| 9 | 2 Abr | JSP | Verificação dedutiva de algoritmos concorrentes em Why3 |
| 10 | 9 Abr | JSP | Verificação dedutiva de algoritmos de exclusão mútua com passagem de ‘token’ em Why3 |
| 11 | 23 Abr | JSP | Verificação dedutiva de algoritmos distribuídos (com troca de mensagens) em Why3 |
| 12 | 30 Abr | JSP | Refinamento de sistemas de transição em Why3 |
| 13 | 7 Mai | JSP | Verificação de um algoritmo de consenso de blockchain em Why3 |
| 14 | 28 Mai | JSP | 2º Teste |
| 16 Jun | MAC+JSP | Exame |
Material
Apontamentos
- Introdução ao TLA+
- Especificação e verificação de algoritmos concorrentes com TLA+
- Especificação e verificação de algoritmos self-stabilizing com TLA+
- Especificação e verificação de algoritmos distribuídos com TLA+
Pasta partilhada Why3
Exercícios para Avaliação Why3
O segundo teste será substituído pela entrega de (no mínimo) duas formalizações em Why3, de entre os exercícios propostos no final das aulas. Lista-se aqui todas as propostas, para referências (os detalhes podem ser consultados nas notas das aulas):
- Algoritmos concorrentes: algoritmo de exclusão mútua de Peterson [Aula Concurrent Programs]
- 2 threads
- N threads
- Algoritmos de passagem de token: estabilidade do algoritmo auto-estabilizante de Dijkstra sobre array
bidireccional [Aula Token-based Mutual Exclusion]
- versão 1 (apenas dois estados presentes no array)
- versão 2 (possivelmente mais do que dois estados presentes no array)
- Algoritmos distribuídos: Algoritmos de Chang-Roberts com modelo de
rede
- modelo idealizado, sem perdas ou duplicações de mensgagens
- modelo admitindo perda de mensagens
- modelo admitindo duplicação de mensagens
- Refinamento:
- Algoritmo de Chang-Roberts com modelo de rede
- Algoritmos auto-estabilizantes de Dijkstra
Aconselha-se que a escolha recaia sobre dois modelos distintos. Por exemplo, não deverão submeter (apenas!) duas versões do algoritmo de Peterson! Mas se acrescentarem um outro exercício, o facto de enviarem duas versões servirá para valorizar o trabalho (em caso de dúvida sobre a escolha de exercícios não hesitem em enviar email!).
A data para entrega (não muito rígida) será a do segundo teste. Será criada uma entrada para esse efeito no Blackboard.
Testes
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
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.