Projecto Integrado (II)
15-July Milestone
Workshop schedule
Morning:
| Begin | End | Description | External(s) | Medium |
|---|---|---|---|---|
| 10h00 | 10h30 | SIG1 | J.Visser, J.P. Correia | Skype |
| 10h30 | 11h00 | SIG2 | J.Visser, J.P. Correia | Skype |
| 11h00 | 11h30 | Evaluation and coffee break | ||
| 11h30 | 12h00 | CS2 | José Miguel Faria | Teleconf |
| 12h00 | 12h30 | Evaluation | ||
Afternoon:
| Begin | End | Description | External(s) | Medium |
|---|---|---|---|---|
| 14h30 | 15h00 | BSC1 | Brian Larsen | Skype |
| 15h00 | 15h30 | BSC2 | Brian Larsen | Skype |
| 16h00 | 17h00 | Evaluation and coffee break | ||
| 17h00 | 17h30 | G1 | Sally Browning | Skype |
| 17h30 | 18h00 | G2 | Sally Browning | Skype |
| 18h00 | 18h30 | Evaluation | ||
Workshop Skype id: uminho-di-a1
Projectos selecionados
| #Proj | Title | Company | Code | Proponent(s) | Tutor | #Group |
| 1 | Massive Parallel Source Code Analysis | SIG | SIG1 | Joost Visser, Miguel Ferreira, José Pedro Correia | JBB | 1 |
| 2 | Extension of a Java library for binary relational algebra | SIG | SIG2 | Joost Visser, Miguel Ferreira, José Pedro Correia | JNO | 4 |
| 3 | Theme PG: formally-verified Pulse Generator | Boston Scientific | BSC1 | Brian Larsen | MJF (JNO) | 8' |
| 4 | Theme DCM: validated Device Controller-Monitor | Boston Scientific | BSC2 | Brian Larsen | LSB (JNO) | 2' |
| 7 | Modelação em NUSMV de um DHSW | Critical Software | CS2 | J.M. Faria, J. Esteves | JSP | 5 |
| 8 | Elliptic curve crypto (ECC) in Cryptol | Galois | G1 | Sally A Browning | MAC | 7 |
| 9 | Cryptol for digital signal properties (DSP) | Galois | G2 | Sally A Browning | MAC | 6 |
Constituição dos grupos:
| Grupo | Número | Nome | PI(II) |
|---|---|---|---|
| Grupo 1 | 15220 | Tiago Veloso | SIG1 |
| 15260 | Luís Couto | ||
| Grupo 2' | 15142 | André Martins | BSC2 |
| 15141 | João Bordalo | ||
| 15395 | Nelson Gonçalves | ||
| Grupo 4 | 15143 | Luís Teixeira | SIG2 |
| 16046 | Márcio Coelho | ||
| Grupo 5 | 15330 | João Martins | CS2 |
| 15753 | André Pedro | ||
| Grupo 6 | 13405 | Manuel Costa | G2 |
| 15345 | Daniel Cadete | ||
| Grupo 7 | 16019 | Diogo Araújo | G1 |
| 15997 | Mário Eiras | ||
| Grupo 8' | 15989 | João Melo | BSC1 |
| 15992 | Inês Prada |
Projecto Integrado (I)
Grupos
| Grupo | Número | Nome | Projecto | Milestone 1 | Milestone 2 |
|---|---|---|---|---|---|
| Grupo 2 | 15142 | André Martins | Modelos de Consistência | 10.5 | 14.0 |
| Grupo 5 | 15753 | André Pedro | Channel Allocation | 13.0 | 15.5 |
| Grupo 6 | 15345 | Daniel Cadete | Controlo de Versões | 16.0 | 14.5 |
| Grupo 7 | 16019 | Diogo Araújo | Journaling File System | 13.5 | 12.5 |
| Grupo 3 | 15992 | Inês Prada | Interval Tree Clocks | 13.0 | 13.5 |
| Grupo 2 | 15141 | João Bordalo | Modelos de Consistência | 10.5 | 14.0 |
| Grupo 5 | 15330 | João Martins | Channel Allocation | 13.0 | 15.5 |
| Grupo 8 | 15989 | João Melo | Sistema de Gestão de Escalas | 14.0 | 11.5 |
| Grupo 1 | 15260 | Luís Couto | Alocação de Turnos | 16.5 | 18.0 |
| Grupo 4 | 15143 | Luís Teixeira | Serviços Académicos | 12.5 | 13.5 |
| Grupo 6 | 13405 | Manuel Costa | Controlo de Versões | 16.0 | 14.5 |
| Grupo 4 | 16046 | Márcio Coelho | Serviços Académicos | 12.5 | 13.5 |
| Grupo 7 | 15997 | Mário Eiras | Journaling File System | 13.5 | 12.5 |
| Grupo 3 | 15395 | Nelson Gonçalves | Interval Tree Clocks | 13.0 | 13.5 |
| Grupo 1 | 15220 | Tiago Veloso | Alocação de Turnos | 16.5 | 18.0 |
Milestone 1
- Objectivos:
- Especificar em Alloy um problema de média dimensão.
- Deadline:
- 10 de Dezembro de 2009.
- Deliverables:
- Modelo Alloy.
- Versão preliminar do relatório a entregar na Milestone 2 (com 10 páginas no máximo).
- Apresentação de 20m no dia 10 de Dezembro de 2009.
Milestone 2
- Objectivos:
- Implementar um protótipo em Java do sistema modelado na Milestone 1.
- Anotar o código com invariantes, pré- e pós-condições em JML.
- Efectuar teste do código por forma a atingir uma cobertura aceitável.
- Deadline:
- 25 de Fevereiro de 2010.
- Deliverables:
- Código Java+JML com os respectivos testes.
- Relatório do trabalho desenvolvido no 1º semestre (com 20 páginas no máximo).
- Apresentação de 20m no dia 25 de Fevereiro de 2010.
Relatórios
Os relatórios deverão seguir o formato seguinte:
\documentclass[a4paper]{article}
\usepackage[portuges]{babel}
\usepackage[latin1]{inputenc}
\usepackage{a4wide}
\begin{document}
\end{document}