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) |
|---|
| pg22796 | André Santos | 14.5 | 8.5 | 10 | 7.5 | 16 |
| pg22840 | Cristiano Sousa | 16.5 | 8.5 | 6 | 8 | 16 |
| pg23205 | Daniel Murta | 18 | 9 | 10 | 8 | 18 |
| | Deise Santana Maia | 6.5 | 6.5 | 4 | 7.5 | 10 |
| pg22766 | Fábio Sousa | 9 | 6.5 | 4 | 0 | 8 |
| pg22811 | Guilherme Rodrigues | 11.5 | 9 | 10 | 8 | 15 |
| pg16334 | José Miguel Magalhães | | 9 | 10 | 8 | |
| pg23208 | José Pinheiro | 8.5 | 6.5 | 7 | 6.5 | 11 |
| pg22808 | Maria João Magalhães | 7 | 9 | 10 | 8 | 14 |
| pg22815 | Nuno Carvalho | 11.5 | 8.5 | 6 | 8 | 14 |
| | Thiago Mendonça Ramos | 8 | 6.5 | 4 | 7.5 | 10 |
| pg22832 | Tiago Guimarães | 12 | 6.5 | 7 | 6.5 | 13 |
| pg22576 | Tiago Ferreira | 12 | 6.5 | 8 | 7.5 | 14 |
| pg22812 | Tiago Jorge | 14 | 9 | 10 | 8 | 16 |
| pg21319 | Victor Miraldo | 16.5 | 8.5 | 10 | 7.5 | 17 |
| pg22577 | Xavier Pinho | 7.5 | 6.5 | 8 | 7.5 | 12 |
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).
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:
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:
