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)