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

2021/22

(Em actualização)

Nesta UC são abordadas técnicas clássicas de verificação de software, quer automáticas quer interactivas, apoiadas na utilização de três das ferramentas mais utilizadas para este fim. As técnicas são estudadas de forma complementar e ilustradas por um conjunto de casos de estudo que incluem programas/algoritmos funcionais, imperativos, e distribuídos.

O programa começa por uma introdução ao assistente de prova Coq e ao sistema de tipos que lhe é subjacente. Trata-se de uma ferramenta muito madura e que tem tido inúmeras aplicações em diversos domínios, nomeadamente na verificação “hard” de software — casos de sucesso de grande repercussão incluem a prova mecanizada do teorema das 4 cores ou a certificação integral de um compilador para a linguagem de programação C.

Segue-se o estudo do verificador Why3, uma ferramenta polivalente que oferece uma linguagem de programação ML e uma lógica de primeira ordem, com tipos indutivos e polimorfismo. As linguagens são integradas de uma forma que suporta a verificação de algoritmos com base em lógica de Hoare, e também a utilização de programas no desenvolvimento de provas ao nível lógico. O Why3 funciona simultaneamente como front-end para as mais variadas ferramentas de prova (incluindo SMT solvers) constituindo desta forma uma plataforma única para a verificação de software baseada, sempre que possível, em prova automática.

Finalmente, a suite TLA+ é também uma ferramenta clássica e de grande repercussão, adoptada em anos recentes na verificação de software altamente complexo por parte de empresas como a Amazon. Apesar de incluir também um núcleo de lógica de primeira ordem e suporte para prova automática, o que distingue esta ferramenta das anteriores é por um lado a utilização de lógica temporal e da noção de “refinamento”, utilizado por exemplo no estabelecimento da relação entre especificações e implementações, e por outro a existência de um “model checker” para a exploração algorítmica (automática) dos estados de um sistema.

Programa

Docentes

Avaliação

Horário

Tipo Horário Sala
Teórica 6ªf. 9h-11h Ed.1 1.19
Teórico-prática 6ªf. 11h-12h Ed.1 1.19

Planificação

# Data Docentes Sumário
1   MJF Dedução Natural. Proposições como tipos. Introdução ao sistema de prova assistida Coq.
2   MJF Tipos indutivos e seus eliminadores. Provas por indução em Coq.
3   MJF Correção de programas funcionais. Extração de programas.
4   MJF Teste laboratorial de Coq.
5   JSP Why3: Lógica e verificação de programas imperativos
6   JSP Why3: Verificação de programas funcionais
7   JSP Why3: Verificação de sistemas distribuídos
8   JSP Why3: Teste
9   MAC Model Checking: estruturas de Kripke, logica temporal linear (LTL), introdução ao nuXmv e TLA+.
10   MAC Model Checking: lógica temporal de tempo ramificado (CTL), LTL vs CTL, safety vs liveness, condições de justiça.
11   MAC Model Checking: verificação explícita de CTL, verificação simbólica de CTL, verificação explícita de LTL.
12   MAC Model Checking: esclarecimento de dúvidas.
13   MAC Model Checking: teste.
    MAC, MJF, JSP Exame.
    MAC, MJF, JSP Projecto.

Material

Slides

Exercícios

Testes

Exemplos

Bibliografia

Outras leituras recomendadas

Ferramentas