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 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:
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:
- Breve introdução aos métodos formais e a técnicas de verificação formal.
- 2 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.
- 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