Construção e Verificação de Software (2017/2018) - Departamento de Informática
Descrição

Esta disciplina ensina princípios, métodos, técnicas e ferramentas para a construção e validação robusta de sistemas de software, de forma a garantir a ausência de erros de programação ("bugs"), com ênfase na programação CONCORRENTE e SEGURA (SAFETY).

São utilizadas ferramentas avançadas, por exemplo as disponibilizadas pela Microsoft Research no siteRISE4FUN, ou Facebook (INFER) e usadas em grandes empresas como a Microsoft, a Amazon e o Facebook.

É uma disciplina indispensável para os estudantes que pretendam dominar técnicas avançadas de construção de software, em particular de software com concorrência e requisitos de segurança, uma mais valia profissional importante.

No fim da disciplina, os estudantes saberão raciocinar de forma clara e precisa sobre a correcção e a segurança do software que desenvolvem, usar ferramentas sofisticadas de análise de software, desenvolver testes e saber interpretá-los, e escrever software usando concorrência.

Exemplo de trabalho final: Em 12/13 os alunos desenvolveram um web-server concorrente completamente certificado para ausência de erros de concorrência, erros de referências nulas e percas de memória.

A linguagem base do curso é JAVA, mas serão usadas também outras linguagens de programação e ferramentas (e.g., JAVASCRIPT, DAFNY, INFER).

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 (verhttp://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.

Programa

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 Principal

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 TutorialJan 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

Requisitos Prévios

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

Esforço do Aluno
  Horas por crédito 28
  Horas p/ semana Semanas Horas
Total de Horas 0
ECTS 6.0