| |
Módulos
A UCE consta dos módulos
- 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
que se articulam entre si da forma seguinte
e cujo programa resumido se apresenta de seguida.
Programas resumidos
Cálculo de Sistemas de Informação
- Motivação: quando é que se pode dizer que um programa está correcto? E que teorias / estratégias / técnicas / ferramentas temos para o garantir?
- Papel da abstracção e da modelação. Modelos e protótipos. Captação de requisitos e sua relação com a interpretação gramatical. Ciclo de desenvolvimento de Balzer.
- Importância dos sistemas de tipos. Limites da tipagem estática. Necessidade de invariantes de tipo. Primeira obrigação de prova: preservação de um invariante.
- 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.
- 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.
- 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).
- "ESC for free'': Regras do cálculo de obrigações de prova.
Análise, Modelação e Teste
- Ciclo de desenvolvimento de software com métodos formais.
- O papel da abstracção na modelação formal.
- Especificação e verificação formal de software: a linguagem de especificação formal Alloy.
- Especificação e verificação formal de sistemas reactivos: model checking de lógica temporal.
- Teste de software: teste unitário e funcional, análise de cobertura, teste orientado aos modelos, geração de testes, injecção de falhas.
- Qualidade de software: métricas de software, normas de codificação e verificação de estilo.
Verificação Formal de Software
- Introdução à verificação formal. 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.
- 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. 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.
- Lambda calculi tipados. Lógica de Ordem Superior. Isomorfismo de Curry-Howard. Sistema de prova assistida Coq. Extracção de programas.
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.
-- JoseNunoOliveira - 13 Sep 2012
|
|
 Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
|
|
| |