Projecto Integrado (II)

Grupos, alunos e temas.

Gr Nome Nr Fotografia Tema
Grupo Critical Software
1 João Silva de Melo pg15989 João Melo ANÁLISE DA PROPAGAÇÃO DE FALHAS EM SISTEMAS COMPLEXOS
Grupo Galois
2a Iago Abal Rivas pg16305 IagoAbal Using quantified rewrite patterns with SMT solvers
2b Jorge Cunha Mendes pg16490 JorgeMendes High Assurance Digitial Signal Processing
Paul van der Walt E4083 Paul van der Walt
Grupo Brazilian Aeronautics and Space Institute
3 Daniel Ribeiro Quinta pg18385 DanielQuinta Safety Critical Interactive Computing Systems’ Modelling
Manuel António Freitas de Sousa pg17297 ManuelSousa
Grupo Primavera Software Factory
4 Leonel João Fernandes Braga pg17311 LeonelBraga Verificação formal de um componente de cálculo do IVA
Rui Miguel de Carvalho Gonçalo pg18378 Rui Goncalo
Grupo Software Improvement Group
5 André Vilas Boas da Costa pg16875 AndreCosta Analysis of OSS projects
Ricardo Daniel Queirós Alves pg17904 RicardoAlves

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 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

  • 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}