Semana

Sumário

Material

1ª

9-13 set

Apresentação da ficha da disciplina.

1. Introdução

O que são os métodos formais. Importância e aplicabilidade dos métodos formais no desenvolvimento de software. Classificação de métodos formais.

Modelo de ciclo de vida e processos de desenvolvimento de software incorporando métodos formais.

Especificação, refinamento, implementação, verificação e validação.

Modelos explícitos vs implícitos, executáveis vs não executáveis.

Técnicas de verificação formal. (Introduction)

2ª

16-20 set

2. Alloy Constraint Analyzer

Modelação declarativa. Comandos Alloy. Funções; predicados; factos; asserções e verificações (checks).

(Alloy1) (Alloy2)

Alloy movie

Alloy tutorial

Exercícios de Alloy (1)

Possible solution (PT)

3ª

23-27 set

2. Alloy Constraint Analyzer

Operadores lógicos; Quantificadores.

Resolução de exercícios.  Exemplo “ceilings and floors”.

Modelação estática vs dinâmica.

(Alloy3) (Alloy4) (example: Grandpa)  

Exames de Alloy de anos anteriores:

(1)

(2)

(3)

Sol2011-10-19

4ª

30 set-4 out

2. Alloy Constraint Analyzer

Simular a execução de uma operação.

Verificar propriedades safety. (Alloy5) (Alloy6)

Exercícios de Alloy

5ª

7-11 out

2. Alloy Constraint Analyzer 

Alloy examples: (Alloy7)

        File System  +   Integers

3. Especificação baseada em modelos (VDM1)

As linguagem VDM-SL e VDM++.

Operações vs funções em VDM++.

Definição de classes, variáveis de instância e operações.

Exercícios de Alloy (2)

6ª

14-18 out

3. Especificação baseada em modelos

Representação de dados com base em estruturas matemáticas (conjuntos, sequências e funções finitas).

Definição de tipos, valores e funções. (VDM2)

A ferramenta VDMTools. (VDM3)

Tutorial VDM++

VDMStack.rar

7ª

21-25 out

3. Especificação baseada em modelos

Funções finitas.

Instruções e expressões. (VDM4)

Design-by-contract: definição de invariantes, pré-condições e pós-condições.

Ligação do VDM++ ao UML. (VDM5)

Exercícios de VDM

8ª

28 out–1 nov

Consistência da especificação: obrigações de prova e teste. (VDM6)

Mini teste de Alloy a 30 de Outubro

Trabalhos práticos de VDM

Grupos

Exercícios de VDM(1)

9ª

4-8 nov

Semana sem aulas

10ª

11-15 nov

3. Especificação baseada em modelos

Descrição de algoritmos, especificações executáveis.

Resolução de exercícios: o exemplo da Vending Machine. (VDM7)

VendingMachine example.

Concorrência em VDM++ (VDM8)

GRUPOSVDM

11ª

18-22 nov

4. Lógica e model checking

Lógica proposicional, de predicados, temporal linear (LTL),

temporal ramificada (CTL).

Propriedades safety, fairness, liveness, universalidade, inevitabilidade, possibilidade, ausência, resposta, precedência. (ModelChecking1)

Resolução de exercícios.  (ModelChecking)

Exercícios de VDM

12ª

25-29 nov

7. Provas formais

Introdução à lógica de Hoare. (Prova Teoremas)

Algumas soluções

13ª

2-6 dez

7. Provas formais

Aplicação da lógica de Hoare à prova de correção de algoritmos.

 (Prova Teoremas)

Lógica de Hoare.

Aplicação da lógica de Hoare à prova de correção de algoritmos.

A ferramenta Jape.

(LogicaHoare)

[Entrega do trabalho prático de VDM++ a 6 de dezembro]

Exercícios de análise de consistência

Exercícios de Model Checking

14ª

9-13 dez

Correção do Miniteste

Exercícios de lógica de Hoare

Soluções Hoare

15ª

16-20 dez

Defesa dos trabalhos práticos

Defesa dos trabalhos práticos