Projecto Integrado (II)

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%).

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%).

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}