Objetivos e enquadramento


No desenvolvimento de sistemas informáticos de software ou hardware é essencial garantir a sua correção em relação à especificação inicial. No ciclo de produção, o tempo gasto em verificação tem levado a indústria a procurar a utilização de métodos formais de verificação em detrimento de métodos ad-hoc baseados em testes/simulação, que dificilmente cobrem todos os casos e não permitem garantir de forma rigorosa a fiabilidade e segurança dos sistemas. A verificação, sendo um imperativo na área dos sistemas críticos e de tempo real, tem vindo a ser estendida a outras áreas dos sistemas informáticos (p.e. ao comércio eletrónico). Neste contexto, a unidade curricular de Verificação Formal de Software tem como objetivo a introdução a técnicas formais de verificação de sistemas informáticos, quer baseadas em modelos (model checking) quer em sistemas dedutivos. Pretende-se que o aluno:

  • em ambas as vertentes, perceba a importância da utilização da lógica e dos sistemas formais no desenvolvimento de sistemas informáticos complexos;
  • seja capaz de modelar sistemas simples e de especificar propriedades utilizando lógicas temporais;

  • seja capaz de anotar programas simples duma linguagem imperativa ou orientada a objetos de modo a garantir propriedades de segurança e propriedades funcionais; e de especificar teorias que permitam a modelação de estruturas mais complexas, cuja correção será demonstrada por um demonstrador automático ou interativo;

  • adquira os princípios básicos das duas técnicas de verificação referidas de modo a permitir-lhe a utilização das ferramentas adequadas de verificação (formal) na sua vida profissional futura ou o desenvolvimento de trabalhos de investigação na área de métodos formais;


Os métodos formais para engenharia de software são muito mais abrangentes do que verificação aqui proposta, incluindo também a especificação, a validação do modelo e o refinamento (implementação). Neste contexto, a expressão correto por construção pode referir-se aos métodos que permitem obter um implementação por refinamento em que a correção é garantida em cada passo ou à utilização de métodos de verificação para ser obtida a mesma garantia. A diversidade de metodologias, de ferramentas existentes, de linguagens, paradigmas de programação e sistemas alvo e as suas complexidades não possibilitam o seu tratamento na presente unidade curricular, a menos duma brevíssima introdução.


Programa e conteúdos


O programa da unidade curricular inclui os seguintes tópicos:

  1. Breve introdução aos métodos formais e a técnicas de verificação formal.
  2. Verificação por model checking de sistemas reativos
    • Introdução ao model checking.
    • Modelação de sistemas paralelos: sistemas transição
    • Paralelismo e comunicação
    • Propriedades temporais lineares: segurança, liveness e fairness
    • Propriedades regulares
    • Lógicas temporais: linear (LTL) e ramificada (CTL e CTL*).
    • Modelação e especificação usando um model checker
    • Algoritmos de model checking para LTL e CTL
    • Model checking simbólico: BDDs e OBDDs.
    • Técnicas de implementação de model checking.
    • Algoritmos de decisão baseados em autómatos
  1. Verificação de Dedutiva de Programas
    • Cálculos de correção parcial e total (Lógicas de Hoare).
    • Pré-condições mais fracas e algoritmos de geração de condições de verificação.
    • Verificação de segurança e verificação funcional.
    • Ferramentas para a especificação, verificação e certificação de programas imperativos: geradores de condições de verificação.