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).
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.
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)
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
Experiência de programação com conhecimento básico de programação com objectos, estruturas de dados e lógica elementar.
Horas por crédito | 28 | ||
Horas p/ semana | Semanas | Horas | |
Total de Horas | 0 | ||
ECTS | 6.0 |