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

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

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.