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:
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 iimplementaçã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:
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;
- conheça as principais técnicas e plataformas atuais de demonstração de teoremas quer automáticos quer interativos.
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 iimplementaçã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:
- Breve introdução aos métodos formais e a técnicas de verificação formal.
- Verificação por model checking de sistemas reativos
- Introdução ao model checking.
- Sistemas reativos.
- Lógicas temporais: linear (LTL) e ramificada (CTL e CTL*).
- Modelação e especificação usando um model checker (NUSMV)
- Algoritmos de model checking para CTL.
- Técnicas de implementação de model checking.
- Algoritmos de decisão baseados em autómatos
- Verificação 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.
- Demonstração automática
- Demonstradores automáticos de teoremas baseados em SAT-DPLL e teorias decidíveis: inteiros, reais, arrays, apontadores, etc.
- SMT, algoritmos de decisão e sua combinação.