Projecto Integrado (II)
Grupos, alunos e temas.
Gr | Nome | Nr | Fotografia | Tema |
Grupo Critical Software |
1 | João Silva de Melo | pg15989 | | ANÁLISE DA PROPAGAÇÃO DE FALHAS EM SISTEMAS COMPLEXOS |
Grupo Galois |
2a | Iago Abal Rivas | pg16305 | | Using quantified rewrite patterns with SMT solvers |
2b | Jorge Cunha Mendes | pg16490 | | High Assurance Digitial Signal Processing |
Paul van der Walt | E4083 | |
Grupo Brazilian Aeronautics and Space Institute |
3 | Daniel Ribeiro Quinta | pg18385 | | Safety Critical Interactive Computing Systems’ Modelling |
Manuel António Freitas de Sousa | pg17297 | |
Grupo Primavera Software Factory |
4 | Leonel João Fernandes Braga | pg17311 | | Verificação formal de um componente de cálculo do IVA |
Rui Miguel de Carvalho Gonçalo | pg18378 | |
Grupo Software Improvement Group |
5 | André Vilas Boas da Costa | pg16875 | | Analysis of OSS projects |
Ricardo Daniel Queirós Alves | pg17904 | |
Projecto Integrado (I)
Milestone 1
- Objectivos:
- Especificar em Alloy um problema de média dimensão.
- Deliverables:
- Modelo Alloy (25%).
- Apresentação de 20m no dia 2 de Dezembro de 2010 (10%).
- Arguição da apresentação de outro grupo (5%).
Grupo | Número | Nome | Projecto | Nota |
Grupo 1 | pg16490 | Jorge Mendes | LDAP | 7.25 |
pg18391 | Nuno Oliveira | 7.25 |
Grupo 2 | pg17311 | Leonel Braga | NAnt | 5.25 |
pg18378 | Rui Gonçalo | 5.75 |
| Daniel Quinta | 5.25 |
Grupo 3 | pg16305 | Iago Abal | Darcs | 7.75 |
pg15989 | João Melo | 7.5 |
Grupo 4 | pg17904 | Ricardo Alves | SGBD | 5.75 |
pg16875 | André Costa | 5.5 |
pg17297 | Manuel Sousa | 5.25 |
Milestone 2
- Objectivos:
- Implementar um protótipo do sistema modelado na Milestone 1 segundo a filosofia DbC.
- Efectuar teste do código por forma a atingir uma cobertura aceitável.
- Recolher métricas com o objectivo de avaliar a qualidade
- Deliverables:
- Código, testes e métricas (25%).
- Apresentação de 20m no dia 24 de Fevereiro de 2011 (10%).
- Arguição da apresentação de outro grupo (5%).
- Relatório do trabalho desenvolvido em PI1 (20%).
Relatório
O relatório de PI1 deverá ter 15 páginas no máximo, excluindo anexos, e seguir o template LaTeX apresentado abaixo. Sugere-se a seguinte estruturação de secções:
- Introdução: descrição do problema; descrição informal dos objectivos de verificação; breve apresentação das linguagens / ferramentas a usar na implementação; breve apresentação da estrutura do relatório.
- Modelo Alloy: apresentação das assinaturas e operações mais relevantes, justificando as opções tomadas; enumeração dos invariantes, factos e asserções mais relevantes; resultados da verificação.
- Implementação: descrição da metodologia usada para refinar o modelo para código; apresentação dos contratos e invariantes mais relevantes.
- Teste e Qualidade do Código: descrição da metodologia de testes utilizada; análise da cobertura dos mesmos; descrição das métricas utilizadas e avaliação da qualidade do código fonte.
- Conclusões: sintetizar os resultados positivos e negativos mais relevantes; avaliação crítica das linguagens e ferramentas utilizadas (incluindo sugestões de melhoria); breve comparação com outras formalizações do mesmo problema.
\documentclass[a4paper]{article}
\usepackage[portuges]{babel}
\usepackage[latin1]{inputenc}
\usepackage{a4wide}
\begin{document}
\end{document}