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

VF/2022-23

Verificação Formal

2022/23

Nesta UC são abordadas técnicas clássicas de verificação automática de software, quer ao nível do design (algoritmos) quer ao nível da implementação (programas). Os casos de estudo a abordar incluem programas e algoritmos imperativos, concorrentes e distribuídos.

Na primeira parte da programa será abordada a verificação de algoritmos, começando com uma breve introdução à verificação de algoritmos imperativos com o Why3, uma ferramenta polivalente que, entre outras técnicas, permite a verificação de algoritmos com base em lógica de Hoare. 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.

Depois será abordada a verificação de algoritmos concorrentes e distribuídos usando TLA+, uma linguagem clássica de grande repercussão, adotada 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 da anterior é 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.

Na segunda parte do programa será abordada a verificação de programas, mais concretamente programas escritos em C. Nesta parte serão utilizadas as ferramentas CBMC e Frama-C.

CBMC é um Bounded Model Checker para programas C e C++. É uma ferramenta automática cuja ideia chave é codificar comportamentos limitados do programa e da propriedade que se quer verificar como uma fórmula lógica, que é depois enviada para um SAT solver. Eventuais modelos dessa fórmula descrevem um traço do programa que leva à violação da propriedade. No entanto, o resultado pode ser inconclusivo se a fómula for insatisfazível. O CBMC verifica problemas de segurança (por exemplo, memory safety, overflow, divisão por zero) e asserções colocadas pelo utilizador, sendo muito bem sucedido na deteção de bugs.

O Frama-C é uma ferramenta de análise que permite verificar formalmente o código C. É uma plataforma modular que suporta vários plugins que implementam diferentes técnicas de análise. A ANSI-C Specification Language (ACSL) usada pelos diferentes plugins, permite a colaboração de análises sobre o mesmo código. Veremos os plugins WP (“Weakest Precondition”) para verificação dedutiva, que permite comprovar o cumprimento dos contratos ACSL por todas as possíveis execuções do código e o RTE (“RunTime Errors”) que gera anotações no código para proteger contra erros de execução. O plugin WP é baseado no weakest precondition calculus, e gera condições de verificação que são depois enviadas a solvers externos (SMT solvers ou sistemas de prova assistida) para finalizar a avaliação das propriedades desejadas. A maioria dos solvers são invocados via Why3.

Programa

Docentes

Avaliação

Horário

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

Planificação

# Data Docentes Sumário
1 17 Fev MAC Algoritmos vs programas. Verificação dedutiva de algoritmos com Why3.
2 24 Fev MAC Modelação de algoritmos com sistemas de transição de estados. Introdução à lógica temporal e ao model-checking explícito.
3 3 Mar MAC Introdução ao TLA e ao TLA+. Introdução à ferramenta TLA+ Toolbox.
4 10 Mar MAC Realização de exercícios.
5 17 Mar MAC Verificação de propriedades de liveness. Especificação de algoritmos distribuídos com TLA+.
6 24 Mar MAC Especificação de propriedades com variáveis de história. Introdução ao refinamento de algoritmos.
7 31 Mar MAC Teste
8 14 Abr MJF Introdução ao “bounded model checking” de software: princípios e algoritmo de transformação de um programa imperativo (anotado com propriedades) num problema de satisfazibilidade. A ferramenta CBMC: modo de funcionamento e análise de casos de estudo para propriedades de “safety”.
9 21 Abr MJF Modelação com CBMC: “nondet_int”, “assume”, e “assert”. Propriedades de “safety” e propriedades funcionais. Casos de estudo. Resolução de exercícios.
10 28 Abr MJF Mecanização da lógica de Hoare. Uma arquitectura para a verificação dedutiva de programas. Weakest precondition calculus. Introdução à plataforma Frama-C para análise estática de código C. Apresentação do plugin WP baseado na lógica de Hoare e no cálculo da pré-condição mais fraca. Experimentação e análise de diversos casos de estudo.
11 5 Mai MJF Prova de correção de programas com ciclos usando o plugin WP do Frama-C. Resolução de exercícios.
  12 Mai   Enterro da gata
12 19 Mai MJF Definição em ACSL de novos predicados e funções lógicas: definições explicitas, definições axiomáticas e definições indutivas. Funções híbridas e predicados híbridos. Introdução de lemas. Análise de diversos casos de estudo. Resolução de exercícios.
13 26 Mai MJF Teste
  21 Jun MAC, MJF Exame

Material

Slides

Exercícios

Exemplos

Bibliografia

Ferramentas