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%)