MFP

Logo

Í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

Docentes

Avaliação

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 Uma máquina de estados para o concept ToDo em Coq
  15 Mai MJF 2º Teste
  5 Jun MAC+JSP+MJF Exame

Material

Exercícios

Exemplos

Bibliografia

Outras leituras recomendadas

Ferramentas