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 2013. 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
E	pg22577	Xavier Pinho	uces.als	Z
A	pg21319	Victor Miraldo	uces.als	UML+OCL
H	pg22812	Tiago Jorge	conferencia.als	B
F	pg22832	Tiago Guimarães	conferencia.als	Z
E	pg22576	Tiago Ferreira	uces.als	Z
G		Thiago Ramos	uces.als	B
C	pg22815	Nuno Carvalho	uces.als	VDM
H	pg22808	Maria João Magalhães	conferencia.als	B
F	pg23208	José Pinheiro	conferencia.als	Z
H	pg16334	José Miguel Magalhães	conferencia.als	B
B	pg22811	Guilherme Rodrigues	conferencia.als	UML+OCL
D	pg22766	Fábio Esteves	conferencia.als	VDM
G		Deise Santana Maia	uces.als	B
B	pg23205	Daniel Murta	conferencia.als	UML+OCL
C	pg22840	Cristiano Sousa	uces.als	VDM
D	pg22759	Celso Silva	conferencia.als	VDM
A	pg22796	André Santos	uces.als	UML+OCL

Exercício sobre Model Checking

No artigo em que propôs o algoritmo para exclusão mútua entre 2 processos, Peterson propôs também uma generalização simples para n processos. Esta generalização garante a exclusão mútua, mas, infelizmente, não garante incondicionalmente a ausência de starvation quando n > 2. Usando o NuSMV modele este algoritmo e tente encontrar um contra-exemplo para essa propriedade.

Este exercício será realizado em grupos de dois alunos. O prazo de entrega é 31 de Janeiro de 2013. 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 da propriedade que origina o contra-exemplo.

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 Apache 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 3 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 é 30 de Junho de 2013. 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.

Exercício para a primeira aula (não sujeito a avaliação)

Este exercício deverá ser realizado em grupos de 3 alunos e entregue manuscrito durante a aula.

A especificação de modelos de software é um dos ingrediente essenciais desta UC. Dada a vossa formação prévia, presumo que este conceito não seja novo. Responda sucintamente às seguintes questões:

• O que é um modelo?
• Quais são os objectivos da modelação?
• Das linguagens/formalismos que aprendeu qual pensa ser mais adequada a modelar software? Justifique.

Considere os seguintes requisitos para uma agenda eletrônica de um cliente de email (adaptado de [1]):

• A agenda deve associar endereços de email a identificadores curtos mais convenientes de usar.
• Nomeadamente, o utilizador deve poder criar um alias para para um determinado correspondente (um identificador único que permanece igual mesmo que o endereço de email se altere).
• Deve também poder criar um grupo que agrega vários emails, alias ou outros grupos.
• Dado um identificador deve ser possível consultar todos os endereços de mail a ele associados (directa ou indirectamente).
• Todos os identificadores devem estar associados (directa ou indirectamente) a pelo menos um endereço de mail.

Especifique um modelo para esta aplicação usando a linguagem/formalismo que escolheu acima. Acha que o seu modelo cumpre os objectivos que indicou?

[1] Daniel Jackson. Software abstractions: logic, language, and analysis. Revised edition, MIT Press, 2012.

Síntese das soluções: