Construção e Análise de Sistemas de Software
Código
8279
Unidade Orgânica
Faculdade de Ciências e Tecnologia
Departamento
Departamento de Informática
Créditos
6.0
Professor responsável
Luís Manuel Marques da Costa Caires
Horas semanais
4
Total de horas
56
Língua de ensino
Português
Objectivos
Saber:
• Construção de desenvolvimento de software confiável tendo em conta concorrência e segurança
• integração da verificação com os processos de construção de software
• Raciocínio baseado na lógica na verificação e análise de sistemas de software
• Análise estática e de verificação de modelos
• Princípios e técnicas de teste de software
Saber Fazer:
• Especificar, verificar e raciocinar sobre correcção de programas através de asserções lógicas
• Definir especificações comportamentais (invariantes, pre-condições e pós-condições) para implementação de módulos e suas interfaces.
• Conceber e implementar planos de teste.
• Usar métodos de programação rigorosos e técnicas de verificação em programas concorrentes
• Conceber políticas de fluxo de informação e sua verificar com asserções e ferramentas.
• Desenvolver em grupo uma aplicação de média dimensão, estaticamente verificada e testada com um grau de cobertura razoável.
Conteúdo
1. Verificação de Software
Métodos baseados em Asserções e Lógicas de Hoare, Dijkstra, Owicky-Gries e Separação.Inferência de Asserções. Tipos comportamentais. Análise de fluxo de dados, de controle e de sinonímia; 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. Programação Segura
Segurança de fluxos de informação e não-interferência. Segurança baseada nas linguagens. Modelos de programação para controle de acessos. Certificação de código. Ferramentas associadas.
5. Exercícios de Desenvolvimento e Projecto Final
Sequência de desafios de programação. Uso de ferramentas (Dafny, JBoss, Verifast, SPIN; Jif)
Método de avaliação
Teste intermédio 30%
Teste Final 30%
4 pequenos trabalhos práticos 10% cada