Métodos Formais em Engenharia de Software

Mestrado de [Engenharia] Informática (2010/11)

Tópicos

Avisos

27 Jul - A notas finais estão publicadas em Funcionamento.

11 Jul - A notas à data da época normal estão publicadas em Funcionamento.

18 Jun - Teste de VFS terá lugar na 2a.fa. dia 20, às 15:00, na sala 0.02.

16 Jun - Deadline para entrega do relatório (hard): 23-Jun

16 Jun - Atenção ao facto de, para evitar conflito com as JOIN (28-30 Jun), a Milestone 3 (final) terá lugar numa sexta-feira, dia 1-Jul. O escalonamento das apresentações será anunciado no respectivo sumário.

14 Jun - As classificações do teste de CSI podem ser consultadas em Funcionamento.

16 Mar - Informa~se que, devido a um imprevisto de ordem pessoal, o Prof. LSB não poderá dar aula amanhã de manhã.

10 Mar - Informa~se que hoje de tarde só há a sessão às 17h00 (aulas de VFS só na próxima semana)

09 Mar - A alocação de projectos + tutorias de PI(II) serão anunciadas na sessão de amanhã (17h00).

23 Fev - A agenda e acetatos da milestone 2 estão no tópico do projecto.

10 Fev - A workshop de apresentação de propostas de projectos por parte dos parceiros industriais da UCE terá lugar dia 03-Mar, ver Sumários)

10 Fev - A Milestone PI(2) terá lugar dia 24-Fev de manhã; de tarde decorrerá a apresentação dos módulos do 2º semestre)

20 Jan - O dia 3-Fev será integralmente dedicado ao módulo CSI (aulas de revisões e preparação para o teste de 10-Fev)

4 Jan - As notas da primeira milestone de PI1 foram publicadas.

21 Dez - Já estão online os enunciados de mais um mini-projecto e um exercício de leitura de AMT.

14 Dez - Qualidade de dois projectos de MFES (2009/10) analisada na Open Code Clinic da SIG

02 Dez - No dia 16 de Dezembro não haverá sessão de CSI - todo o dia será dedicado a AMT (docente: Joost Visser)

29 Nov - As notas do teste de Alloy foram publicadas na secção AMT.

24 Nov - A primeira milestone do Projecto Integrado terá lugar dia 2-Dez.

28 Set - As aulas da edição corrente da UCE (2010/11) iniciaram-se a 30-Out, às 9h00, na sala DI 1.08 do Departamento de Informática.

29 Set - Criação do site.

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

  • 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. 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

  • Formal methods and the formal method life-cycle.
  • The role of abstraction in formal 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.
  • Software metrics, Codings standards, Style checking.

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.
  • Apresentação e revisão de conceitos básicos da lógica. Os problemas de decisão SAT e a sua complexidade. Sistemas de prova automática e sistemas de prova assistida.
  • 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.
  • Sistemas de tipos e lambda calculi tipados. Apresentação do sistema de tipos de suporte ao sistema Coq: "Calculus of Inductive Constructions" (CIC). Exemplos em Coq de diversas definições indutivas e análise dos recursores gerados pelo sistema.

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.

r2 - 19 Oct 2010 - 14:24:18 - AlcinoCunha
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM