Métodos Formais em Engenharia de Software

• Languages for formal specification and verification of software systems.
• Specification and verification of reactive systems: model checking for temporal logic.

Módulos

A UCE consta dos módulos seguintes,

• CSI - Cálculo de Sistemas de Informação
• AMT - Análise, Modelação e Teste
• VFS - Verificação Formal de Software
• PAS - Processos e Arquitecturas de Software
• PI - Projecto Integrado

cujo programa resumido se apresenta de seguida:

Cálculo de Sistemas de Informação

• <-- Ciclo de vida de Balzer. !-->

  Modelos e seu papel na concepção de soluções. Protótipos. Captação de requisitos e sua relação com a interpretação gramatical.
• Limites da tipagem estática. Necessidade de invariantes de tipo.

  <-- Significado de um invariante. !-->

  Primeira obrigação de prova: preservação de um invariante.

  <-- Recurso a quantificações universais e existenciais em invariantes. !-->

• Necessidade de pre-condições para (a) especificação implícita de funções; (b) modelar o indeterminismo da realidade; (c) modelar relações; (d) permitir liberalidade ao especificador.
• Pares pre/post: satisfiabilidade. Obrigações de prova: necessidade de uma transformada para a lógica e teoria de conjuntos. Transformada PF.

  <-- : eliminação de quantificadores por introdução de relações binárias. !-->

• Estudo do cálculo de relações binárias. Relações simples e relações co-reflexivas. Representação de conjuntos por co-reflexivas.
• "Extended Static Checking" (ESC) usando a transformada-PF. Caso de estudo em verificação estática estendida: o VFS (Verified File System).
• Propriedades expressas sob a forma de conecções de Galois.

  <-- Propriedades genéricas destas últimas. !-->

• Polimorfismo funcional versus ESC: tipos vistos como relações. Cálculo da relação associada a um tipo polimórfico. Teorema grátis de uma função polimórfica (ou teorema de Reynolds-Wadler).

  <-- expresso em notação-PF. Noção de relator e suas propriedades. !-->

• "ESC for free'': Regras do cálculo de obrigações de prova.

<-- Relações também como estruturas de dados. Exemplos: listas; tabelas relacionais com chaves primárias. Refinamento de dados: cálculo de esquemas de bases de dados relacionais a partir the modelos abstractos usando o cálculo relacional. !-->

Análise, Modelação e Teste

• Formal methods and the formal method life-cycle.
• The role of abstraction in formal modelling.
• Languages for formal specification and systems modelling.
• The “design-by-contract” approach to software development.
• Unit testing, Functional testing, Test coverage analysis.
• Model-driven testing, Test generation, Model checking, Fault injection.
• Software metrics, Codings standards, Style checking.

Verificação Formal de Software

• Introdução à verificação formal.

  <-- Motivação para o estudo da semântica das linguagens de programação. !-->

  Estudo de uma linguagem imperativa simples. Semântica operacional de transições dada por uma máquina abstracta. Semântica operacional estrutural. Semântica de avaliação. Propriedades e relação entre semânticas.
• Apresentação e revisão de conceitos básicos da lógica.

  <-- A interacção entre a lógica e as ciências da computação. Perspectiva clássica versus intuicionista. Lógica Proposicional e Lógica de Primeira Ordem. !-->

  Os problemas de decisão SAT e a sua complexidade. Sistemas de prova automática e sistemas de prova assistida.
• Lógica de Hoare.

  <-- A propriedade de sub-fórmula e a sua ausência na lógica de Hoare. !-->

  Construção de árvores de prova com base na noção de "pré-condição mais fraca". Uma arquitectura para a verificação de programas.

  <-- : geração de condições de verificação. !-->

  Algoritmo VCGen.
• Estudo do plugin “Jessie'' para verificação dedutiva. O VCGen genérico “Why'' e interface gráfica “Gwhy''. Sua utilização com múltiplas ferramentas de prova automática. A linguagem de anotações ACSL; verificação baseada em contratos.

  <-- Exemplos: tabulação da função factorial; determinação do máximo de um vector. Exercícios: função “swap''. Partição de um array. !-->

• Sistemas de tipos e lambda calculi tipados.

  <-- PTS - caracterização da meta-teoria: sintaxe, especificação, regras de tipagem e principais resultados. Breve descrição do lambda cubo. !-->

  Apresentação do sistema de tipos de suporte ao sistema Coq: "Calculus of Inductive Constructions" (CIC).

  <-- Descrição do CIC como PTS. Análise das dependências de tipos admitidas neste sistema. Tipos indutivos: análise do conceito e das condições para a sua boa fundação. Recursor do tipo indutivo como codificação do princípio de indução estrutural sobre os seus elementos, e regras de computação associadas. Recursividade geral e análise de casos: regras de tipagem e computação associadas. Observações sobre a terminação das funções assim definidas. !-->

  Exemplos em Coq de diversas definições indutivas e análise dos recursores gerados pelo sistema.

  <-- Sessão laboratorial sobre o sistema Coq. !-->

Processos e Arquitecturas de Software

• Introdução aos sistemas reactivos. Motivação e definição base.
• Fundamentos: sistemas, comportamento e coindução.
• Noção de sistema de transição etiquetado e correspondente morfismo. Noção de simulação e bisimulação. Propriedades.
• Modelação de processos em CCS. Sintaxe e semântica operacional. Exemplos. Bissimilaridade e equivalência estrita.
• Cálculo de processos em CCS. Equivalência e igualdade observacional. Leis. O teorema da expansão. Resolução de equações.
• Estudo de linguagens para descrição de arquitecturas de software: REO e ORC.

Projecto Integrado

Nestas horas lectivas os alunos realizam, em grupo, projectos propostos pelas empresas que patrocinam a UCE, previamente apresentados pelos proponentes numa workshop interna que dá início ao processo. No decorrer do projecto há visitas dos alunos às instalações das empresas sempre que tal é conveniente. No final do ano, o PI fecha-se com uma outra workshop em que os grupos apresentam os seus resultados aos docentes e staff das empresas (por video-conferência, se necessário), participando estes últimos também na sessão de avaliação final.