Construção e Verificação de Software

Objetivos

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.

Caracterização geral

Código

11159

Créditos

6.0

Professor responsável

Bernardo Parente Coutinho Fernandes Toninho, Luís Manuel Marques da Costa Caires

Horas

Semanais - 4

Totais - 52

Idioma de ensino

Inglês

Pré-requisitos

.

Bibliografia

Dafny Guide : http://dafny.org/latest/DafnyRef/DafnyRef

"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 ensino

As aulas teóricas introduzem os vários tópicos centrais na unidade curricular. Lógica de Hoare, Lógica de Separação e a respectiva utilização em ferramentas de verificação de software.

As aulas de laboratório consistem na utilização de ferramentas de verificação estática de software a código imperativo, primeiro com exercícios de laboratório, e depois com código mainstream, com potencial aplicação real. A unidade curricular inclui o desenvolvimento de um projeto utilizando linguagens  mainstream.

Método de avaliação

A avaliação consiste de duas componentes: componente teórico-prática e componente prática.

A componente teórico-prática tem um peso de 60% na nota final e uma nota mínima de 9,5 valores, e consiste em dois testes com igual peso, ou um exame. Os testes e o exame são presenciais. Os testes e o exame é são sem consulta.

A componente prática tem um peso de 40% e uma nota mínima de 9,5 para obter frequência, correspondendo a 3 exercícios de especificação e verificação, de igual peso na nota. Os exercicios devem ser realizados em grupos de 2 alunos e as notas estão sujeitas a eventual discussão.

Todas as notas são arredondadas às décimas, excepto a nota final que é arredondada às unidades.

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)

Cursos

Cursos onde a unidade curricular é leccionada: