Objectivos da disciplina e tópicos do programa. Métodos de avaliação. Bibliografia recomendada.
Breve introdução aos métodos formais para o desenvolvimento de sistemas informáticos.
Introdução ao Model checking. Sistemas de transição. Execuções. Modelação de circuitos sequências e programas.
Breve introdução aos métodos formais para o desenvolvimento de sistemas informáticos.
Introdução ao Model checking. Sistemas de transição. Execuções. Modelação de circuitos sequências e programas.
Aula 3/4 1/03
Paralelismo e Comunicação. Grafos de Programa. Concorrência e Intercalagem. Comunicação por variáveis partilhadas. Protocolos de Exclusão Mútua.
Paralelismo e Comunicação (cont.). Passagem de mensagens síncronas e assíncronas. Sistemas de canais e sistemas de transição associados. Exemplo: protocolo do bit alternado. Produto síncrono. Problema da explosão do número de estados.
Aula 9/10 22/03
Promela e o model checker SPIN. Processos, variáveis partilhadas e canais. Exemplos de verificação de programas sequenciais e concorrentes
Bibliografia: PMCSPIN Cap 1-4 e Cap 7
Aula 11/12 29/03
Tempo linear e ramificado. Lógica Temporal Linear. Semântica duma fórmula dado um sistema de transições. Satisfabilidade ao longo de um traço, dum caminho, num estado e num sistema. Equivalência de fórmulas. Especificação de propriedades usando fórmulas LTL. Especificação de assunções de justeza (fairness).
Bibliografia: Cap 5.1- PMC
Aula 13/14 12/04
Lógica Temporal Ramificada:CTL, lógica de árvores de computação. Semântica duma fórmula dado um sistema de transições. Satisfabilidade num estado e num sistema. Equivalência de fórmulas. Especificação de propriedades usando fórmulas CTL. Comparação entre LTL e CTL. CTL*.
Bibliografia: Cap 6.1—6.3, 6.8.1 PMC
Exercícios:
Aula 15/16 26/04
Algoritmo de etiquetagem para o model checking do CTL. Optimização usando a conectiva EG. Correção e terminação do algoritmo: funções monótonas e pontos fixos mínimos e máximos. Teorema de Knaster-Tarski. Correção das funções SAT_EG, SAT_AF e SAT_EU.
Bibliografia: LICS Cap pp 221-232, 238-245, PMV Cap 6.4
Aula 17/18 3/05
Model checking simbólico. Definição de BDDs (binary decision diagrams). OBDDS: BDDs reduzidos e ordenados. Propriedades dos OBDDs. Algoritmos para a Construção de BDDS reduzidos. Expansão de Shannon para funções booleanas. Algoritmos apply, restrict e exists. Representação de conjuntos finitos com OBDDs. Representação de um modelo em OBDDs: conjunto de estados e relação de transição. Operações necessárias para o algoritmo de etiquetagem. Síntese de OBDDs.
Bibliografia: LICS Cap 6 pp 358-388 PMC Cap. 6.7.1, 6.7.3
Verificação de programas baseado em sistemas dedutivos. Lógicas de Floyd-Hoare baseadas em pré e pós condições. Correcção parcial e correcção total. Uma linguagem imperativa simples. Asserções e linguagem das condições. Sistema dedutivo para a correcção parcial. Exemplos. Pre-condições fracas para o cálculo de correcção parcial. Tableaux para o sistema dedutivo para a correcção parcial. Invariantes de ciclo.
Sistema dedutivo para a correcção parcial (cont.) Uma semântica operacional para a linguagem While. Integridade do sistema de correcção parcial. Cálculo de correção total. Variantes estritamente decrescentes. Regra para o comando while.
Bibliografia:LICS Cap 4.1-4.3.2 , RSD cap 5.1-5.6
Regras da Lógica de Hoare
Linguagem de anotações Dafny
Regras da Lógica de Hoare
Linguagem de anotações Dafny
Bibliografia: Cap 2.2.1-2.2.2 PMC
Uma arquitectura de um sistema de verificação de programas: mecanização do processo de dedução na lógica de Hoare. Lógica de Hoare orientada a objectivos. Pré-condições mais fracas. Algoritmo de geração de condições de verificação (VCGens) para a linguagem While com inteiros. Lógica de Hoare para Arrays. Propriedades de segurança. Uma semântica operacional para a linguagem While com inteiros considerando a noção de erro. Lógica de Hoare com condições de segurança. Algoritmo de geração de condições de segurança. Breve introdução à plataforma Dafny. Exemplos