Guia de Cursos

Queres conhecer a oferta de cursos da NOVA, nas áreas das licenciaturas, mestrados e doutoramentos?
No nosso Guia de Cursos encontras informação útil sobre Faculdades, Institutos e Escolas.
Podes ainda aceder a informações complementares necessárias a uma completa integração.

saber mais Guia de Cursos

Faculdade de Ciências e Tecnologia

Construção e Verificação de Software

Código

11159

Unidade Orgânica

Faculdade de Ciências e Tecnologia

Departamento

Departamento de Informática

Créditos

6.0

Professor responsável

João Ricardo Viegas da Costa Seco, Luís Manuel Marques da Costa Caires

Horas semanais

4

Língua de ensino

Português

Objectivos

Saber:

Os alunos consolidam as aptidões de construção de desenvolvimento de software confiável, no contexto dos modernos sistemas, onde a concorrência e a segurança desempenham um papel crucial. 

A UC desenvolve o ponto de vista de que a verificação dever ser integrada de forma coesa com os processos de construção de software, orientada pelo uso de ferramentas de análise de código, como as disponibilizadas pela Microsoft Research (ver http://rise4fun.com).

São cobertas as técnicas fundamentais de análise estática e de verificação de modelos, assim como princípios e técnicas de teste de software.

Saber Fazer

Usar métodos de programação rigorosos e técnicas de verificação para garantir a fiabilidade de programas concorrentes baseados em monitores (usando java.util.concurrent) e transações.

Desenvolver, em trabalho de grupo, o projecto de uma aplicação de média dimensão, estaticamente verificada e testada com um grau de cobertura razoável.

Usar asserções lógicas para especificar, verificar e raciocinar sobre a correcção de programas, assim como as ferramentas associadas (DAFNY, VERIFAST, JIF).

Definir fluentemente especificações comportamentais (invariantes, pre-condições e pós-condições) para a implementação de módulos e suas interfaces.

Conceber e implementar planos de teste.

Pré-requisitos

Experiência de programação com conhecimento básico de programação com objectos, estruturas de dados e lógica elementar.

Conteúdo

1. Construção Verificada de Software

Métodos baseados em Asserções e Lógicas de Hoare e Separação.Inferência de Asserções. Tipos Abstractos e Tipos comportamentais; Invariantes de Representação. Interpretação Abstracta. Verificação de Modelos. Ferramentas associadas.

2. Teste de Software

Testes baseado em Modelos e Falhas. Selecção e Geração de Testes. Execução Simbólica. Ferramentas associadas.

3. Programação Concorrente

Partilha, Confinamento, Posse. Controle de Interferência. Verificação de código com monitores e semáforos usando invariantes de recursos. Controle de concorrência a partir de especificações comportamentais.

4. Exercícios de Desenvolvimento e Projecto Final

Sequência de desafios de programação. Uso de ferramentas (Dafny, JBoss, Verifast, SPIN; INFER)

Bibliografia

Dafny Guide : http://rise4fun.com/Dafny/tutorial/guide

"Program Development In Java: Abstraction, Specification, And Object-Oriented Design". Liskov/Guttag; MIT Press.

Java Concurrency in Practice, Goetz et al. Addison-Wesley, 2006.

VeriFast for Java: A Tutorial Jan Smans, Bart Jacobs, and Frank Piessens (http://people.cs.kuleuven.be/~bart.jacobs/verifast/verifast-java-tutorial.pdf).

Language Based Information Flow Security, A. Sabelfeld, A. C. Myers, 2004.

Several classical papers by Liskov, Hoare, Dijkstra, Brinch Hansen, Doug Lea, O’Hearn, Schneider.

Related course ar MIT: http://ocw.mit.edu/courses/electrical-engineering-and-computer-science/6-005-elements-of-software-construction-fall-2011/index.htm

Método de avaliação

Teste intermédio 40%

Teste Final 40%

4 pequenos trabalhos práticos 5% cada

Os primeiros dois trabalhos estão integrados num só (que valerá 10%)

Cursos