Aula 1/2 16/02
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 5/6 02/03
Paralelismo e Comunicação (cont.). Passagem de mensagens síncronas e assíncronas. Sistestemas de canais e sistemas de transição associados. Produto síncrono. Problema da explosão do número de estados. Introdução à linguagem Promela e ao model Checker SPIN.
Bibliografia: Cap 2.2.4-2.2.7 PMC; PMCSPIN
Aula 9/10 16/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 11/12 23/03
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
Aula 13/14 7/04
Conjunto completo de conectivas para o CTL. 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. Model checking com fairness (justeza).
Bibliografia: LICS Cap pp 221-232, 238-245, PMV Cap 6.4
Aula 15/16 13/04
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
Aula 17/18 27/04
Autómatos finitos não determinísticos e autómatos finitos de Büchi. Autómatos Finitos Alternados. Autómatos de Büchi alternados. Autómato de Büchi e Autómato de Büchi alternado associados a uma fórmula do LTL, AF. Autómato de Büchi associado a um modelo. Algoritmo de model checking para o LTL.
Bibliografia: Automata-Theoretic Approach to LTL, M. Vardi
PMC Cap 5.2 (usando Autómatos de Buchi Generalizados)
PMC Cap 5.2 (usando Autómatos de Buchi Generalizados)
Continuação da aula anterior. 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.
Bibliografia:LICS Cap 4.1-4.3.2 , RSD cap 5.1-5.4
Exercícios:
Sistema dedutivo para a correcção parcial. 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.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
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. 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 frama-C, WP e linguagem de especificação ACSL. Exemplos