Objetivos da Unidade Curricular

Pretende-se que o aluno fique a conhecer as principais técnicas sistemáticas (métodos formais) e ferramentas que, correntemente, podem ser usadas no processo de desenvolvimento de software de forma a aumentar a fiabilidade dos sistemas desenvolvidos. A ênfase será essencialmente em instrumentos que permitem verificar a correcção dos sistemas desenvolvidos relativamente aos requisitos para os quais foram concebidos. Pretende-se ainda que o aluno seja capaz de utilizar as seguintes ferramentas: JML, ESC/Java2, Spin.

---

Pré-requisitos

• Lógica de Primeira Ordem (12841)
• Desenvolvimento Centrado em Objetos (26727)

---

Conteúdos

1. Fiabilidade de sistemas de software: problemas, desafios e soluções.
2. Verificação dedutiva de programas: cálculo de Hoare.
3. JML: The Java Modeling Language.
4. ESC/Java2: The Extended Static Checker for Java.
5. Verificação automática de modelos.

 

---

Descrição detalhada dos conteúdos programáticos

Componente Teórica

1. Fiabilidade de sistemas de software: problemas, desafios e soluções.
2. Verificação dedutiva de programas

2.1 Cálculo de Hoare.
3. Especificação de propriedades em JML (Java Modeling Language)

3.1 Design by Contract
3.2 Especificação baseada em propriedades
3.3 Especificação baseada em modelos
4 Verificação estática estendida

4.1. ESC/Java
5. Verificação automática de modelos

5.1 Modelação de SIstemas

5.2 Especificação com Lógica Temporal Linear (LTL)

5.3 Verificação de modelos para LTL

5.4 SPIN

 

Componente Teórica-Prática

2. Verificação dedutiva de programas: cálculo de Hoare.

   -- Exercícios de dedução. Padrões de dedução. 

3. Especificação com JML

    --Exemplos e exercícios: como introduzir anotações em programas, 
       como verificar programas com um compilador para programas anotados 
       com contratos em JML. 

4. Análsei Estática Estendida

4.1 ESC/Java2

    -- Exemplos e exercícios: como usar o compilador ESC/Java2 ,

5. Verificação automática de modelos.

    -- Exemplos e exercícios: SPIN model checker.

 

Componente Prática

Trabalhos em verificação dedutiva de software, Dafny, Java Modeling Language, ESC/Java, e SPIN.

 

---

Bibliografia

Recomendada

Doron Peled, Software Reliability Methods, Springer, 2001.
Mordechai Ben-Ari, Principles of the Spin Model Checker, Springer 2008
Gerard Holzmann, Spin Model Checker: Primer and Reference Manual, Addison Wesley, 2003
Program Development in Java. Barbara Liskov with John Guttag, Addison Wesley, 2001

 

Outros elementos de estudo

Overview research papers on JML and ESC/Java

 

---

Métodos de Ensino

1 aula semanal de 3,5h.
Três trabalhos.

 

---

Métodos de Avaliação

3 trabalhos (40%)
exame final (60%)

 

---

Língua de ensino

Português ou Inglês