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.
- Deadline:
- 28 de Novembro de 2010.
- 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 3 | pg16305 | Iago Abal | Darcs | 7.75 |
| Grupo 3 | pg15989 | João Melo | Darcs | 7.5 |
| Grupo 1 | pg16490 | Jorge Mendes | LDAP | 7.25 |
| Grupo 1 | pg18391 | Nuno Oliveira | LDAP | 7.25 |
| Grupo 2 | pg17311 | Leonel Braga | NAnt | 5.25 |
| Grupo 2 | pg18378 | Rui Gonçalo | NAnt | 5.75 |
| Grupo 2 | Daniel Quinta | NAnt | 5.25 | |
| Grupo 4 | pg17904 | Ricardo Alves | SGBD | 5.75 |
| Grupo 4 | pg16875 | André Costa | SGBD | 5.5 |
| Grupo 4 | pg17297 | Manuel Sousa | SGBD | 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
- Deadline:
- 20 de Fevereiro de 2011.
- 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%).
| Grupo | Número | Nome | Projecto | Apresentação | Arguente | Nota |
|---|---|---|---|---|---|---|
| Grupo 1 | pg16490 | Jorge Mendes | LDAP | 10:00 | Grupo 2 | 9 |
| Grupo 2 | pg17311 | Leonel Braga | NAnt | 10:30 | Grupo 3 | 9.5 |
| pg18378 | Rui Gonçalo | 9.5 | ||||
| Daniel Quinta | 9.5 | |||||
| Grupo 3 | pg16305 | Iago Abal | Darcs | 11:00 | Grupo 4 | 11.75 |
| Grupo 4 | pg17904 | Ricardo Alves | SGBD | 11:30 | Grupo 5 | 9 |
| pg16875 | André Costa | 9 | ||||
| pg17297 | Manuel Sousa | 9 | ||||
| Grupo 5 | pg15989 | João Melo | Darcs | 12:00 | Grupo 1 | 7.5 |
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}