Métodos Formais em Engenharia de Software

Mestrado de [Engenharia] Informática (2010/11)
View   r2  >  r1  ...

Programa 2 - 19 Oct 2010 - Main.AlcinoCunha
Line: 1 to 1
 
META TOPICPARENT name="Funcionamento"

Módulos

Line: 34 to 34
 
  • Formal methods and the formal method life-cycle.
  • The role of abstraction in formal modelling.
Changed:
<
<
  • Languages for formal specification and systems modelling.
>
>
  • Languages for formal specification and verification of software systems.
  • Specification and verification of reactive systems: model checking for temporal logic.
 
  • The “design-by-contract” approach to software development.
  • Unit testing, Functional testing, Test coverage analysis.
  • Model-driven testing, Test generation, Model checking, Fault injection.

Programa 1 - 30 Sep 2010 - Main.AlcinoCunha
Line: 1 to 1
Added:
>
>
META TOPICPARENT name="Funcionamento"

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.

META FILEATTACHMENT attachment="mfes.png" attr="h" comment="" date="1285834062" name="mfes.png" path="mfes.png" size="16938" stream="mfes.png" user="Main.AlcinoCunha" version="1"

Revision 2r2 - 19 Oct 2010 - 14:24:18 - AlcinoCunha
Revision 1r1 - 30 Sep 2010 - 08:07:43 - AlcinoCunha
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM