Análise, Modelação e Teste

Método de Avaliação

A nota do módulo de AMT será a média pesada dos seguintes componentes:

• Teste individual sobre Alloy (40%).
• 1 exercício sobre Linguagens de Modelação (20%).
• 1 exercício sobre Model Checking (20%).
• 1 mini-projecto sobre Qualidade e Teste de Software (20%).

Notas

Número	Nome	Alloy (0-20)	LM (0-10)	MC (0-10)	QTS (0-10)	Final (0-20)
pg19643	Ana Catarina Pereira Correia	14.5	7	7.5	7.5	15
pg25335	Ana Paula Martins Carvalho	15	7	7.5	7.5	15
pg25300	Damien da Silva Vaz	5	6.5	9	7	11
pg26119	Fábio André Martins Fernandes	12.75	5.5	8.5	7	14
pg22766	Fábio Esteves Sousa	15.5	8.5	10	9	17
pg25299	Helder Cristiano Dias Afonso	9	7.5	8.5	8	13
pg26133	João Carlos Alves Cruz	13.75	7.5	8.5	8	15
pg25285	Jorge Lobo Teixeira Lopes	8.5	8.5	8.5	8	13
pg25311	Luís Miguel Pereira Romano	18.25	9	8	8.5	18
a62148	Miguel Ângelo Gomes da Costa	10	8.5	10	9	15
pg25313	Nuno Miguel da Costa Laranjo	12.5	7.5	7	7	14
pg25332	Paulo Alexandre Ribeiro Silva	8.25	8.5	8.5	8	13
pg25318	Rogério António da Costa Pontes	13.5	7.5	7	7	14
pg25263	Telma Ferreira Correia	10.75	5.5	8.5	7	13
pg25301	Vitor Manuel Parreira Pereira	15.25	9	8	8.5	16
pg25340	Yoan David Ribeiro	11.5	6.5	9	7	14

Exercício sobre Linguagens de Modelação

O objectivo deste exercício é estudar uma linguagem de modelação formal alternativa ao Alloy. Este exercício será realizado em grupos. O prazo de entrega é 31 de Janeiro de 2014. Até esta data deverão submeter por email para o docente responsável:

• Um modelo formal equivalente ao exemplo em Alloy atribuído ao grupo.
• Um parágrafo sintetizando as maiores diferenças a nível da linguagem (sintaxe, semântica, sistema de tipos, bibliotecas, etc) entre o Alloy e a linguagem atribuída ao grupo.
• Um parágrafo sintetizando o suporte que a linguagem atribuída ao grupo possui em termos de ferramentas para validação / verificação (nomeadamente, descrevendo se é possível efectuar os comandos presentes no exemplo, para verificação de consistência do modelo ou verificar uma determinada propriedade).

Grupo	Número	Nome	Exemplo	Linguagem
A	pg25313	Nuno Laranjo	uces.als	Eiffel
	pg25318	Rogério Pontes
B	pg19643	Catarina Correia	uces.als	Z
	pg25335	Ana Carvalho
C	pg22766	Fábio Esteves	uces.als	B
		Miguel Costa
D	pg25340	Yoan Ribeiro	uces.als	JML
	pg25300	Damien Vaz
E	pg25285	Jorge Lobo	uces.als	VDM
	pg25332	Paulo Silva
F	pg25301	Vitor Pereira	conferencia.als	Code Contracts
	pg25311	Luís Romano
G	pg25299	Helder Afonso	uces.als	UML+OCL
	pg26133	João Carlos Alves Cruz
H	pg26119	Fábio Fernandes	conferencia.als	UML+OCL
	pg25263	Telma Correia

Exercício sobre Model Checking

O objectivo deste projecto é modelar o algoritmo de exclusão mútua de Szymanski e verificar que propriedades típicas de algoritmos deste tipo satisfaz. No mínimo devem verificar se satisfaz a exclusão mútua e a ausência de starvation. Como este é um algoritmo genérico para N processos, devem modelar uma versão do algoritmo com N>2.

Este exercício será realizado em grupos de dois alunos. O prazo de entrega é 26 de Fevereiro de 2014. Até esta data deverão submeter por email para o docente responsável o ficheiro SMV com o modelo do algoritmo e a especificação das propriedades.

Mini-projecto sobre Qualidade e Teste de Software

O objectivo deste projecto é analisar a qualidade de software de um projecto open-source de média/grande dimensão. Mais concretamente, pretende-se analisar a vertente de maintainability segundo o modelo proposto pela SIG nas seguintes publicações:

• I. Heitlager, T. Kuipers, and J. Visser. A Practical Model for Measuring Maintainability, In proceedings of the 6th International Conference on the Quality of Information and Communications Technology (QUATIC 2007), pages 30-39, IEEE Computer Society Press, 2007.
• J. Visser. SIG/TÜViT Evaluation Criteria Trusted Product Maintainability. Version 4.2. 2012

Para efeitos de comparação, este ano vamos restringir-nos a projectos cuja implementação seja maioritariamente feita em Java. Uma lista dos potenciais projectos pode ser encontrada em http://www.ohloh.net/orgs/apache/projects. Este mini-projecto deverá ser realizado em grupos com no máximo 2 alunos. Cada grupo deverá analisar um projecto diferente: as escolhas e constituição dos grupos serão publicados nesta página e deverão ser comunicados logo que possível ao docente responsável. O prazo de entrega é 31 de Março de 2014. Até esta data deverão submeter por email o relatório com a análise efectuada (max 3 páginas), onde, para além da análise global, deverão também procurar identificar os componentes mais críticos e, na medida do possível, apresentar razões que justifiquem a nota obtida.

Grupo	Número	Nome	Projecto
A	pg25313	Nuno Laranjo	http://www.ohloh.net/p/apache-isis
	pg25318	Rogério Pontes
B	pg19643	Catarina Correia	http://www.ohloh.net/p/CloudStack
	pg25335	Ana Carvalho
C	pg22766	Fábio Esteves	http://www.ohloh.net/p/droids
		Miguel Costa
D	pg25340	Yoan Ribeiro	http://www.ohloh.net/p/Hadoop
	pg25300	Damien Vaz
E	pg25285	Jorge Lobo	http://www.ohloh.net/p/xerces2-j
	pg25332	Paulo Silva
F	pg25301	Vitor Pereira	http://www.ohloh.net/p/Apache-Commons-Math
	pg25311	Luís Romano
G	pg25299	Helder Afonso	http://www.ohloh.net/p/tomcat
	pg26133	João Carlos Alves Cruz
H	pg26119	Fábio Fernandes	http://www.ohloh.net/p/tomee
	pg25263	Telma Correia