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).
| Grupo | Número | Nome | Exemplo | Linguagem |
|---|---|---|---|---|
| A | pg22796 | André Santos | uces.als | UML+OCL |
| pg21319 | Victor Miraldo | |||
| B | pg23205 | Daniel Murta | conferencia.als | UML+OCL |
| pg22811 | Guilherme Rodrigues | |||
| C | pg22840 | Cristiano Sousa | uces.als | VDM |
| pg22815 | Nuno Carvalho | |||
| D | pg22759 | Celso Silva | conferencia.als | VDM |
| pg22766 | Fábio Esteves | |||
| E | pg22576 | Tiago Ferreira | uces.als | Z |
| pg22577 | Xavier Pinho | |||
| F | pg22832 | Tiago Guimarães | conferencia.als | Z |
| pg23208 | José Pinheiro | |||
| G | Thiago Ramos | uces.als | B | |
| Deise Santana Maia | ||||
| H | pg22812 | Tiago Jorge | conferencia.als | B |
| pg22808 | Maria João Magalhães | |||
| pg16334 | José Miguel Magalhães |
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.
| Grupo | Número | Nome | Projecto |
|---|---|---|---|
| G | Thiago Ramos | http://www.ohloh.net/p/jackrabbit-oak | |
| G | Deise Santana Maia | http://www.ohloh.net/p/jackrabbit-oak | |
| H | pg16334 | José Miguel Magalhães | http://www.ohloh.net/p/cassandra |
| A | pg21319 | Victor Miraldo | http://www.ohloh.net/p/commons-collections |
| E | pg22576 | Tiago Ferreira | http://www.ohloh.net/p/wicket |
| E | pg22577 | Xavier Pinho | http://www.ohloh.net/p/wicket |
| A | pg22796 | André Santos | http://www.ohloh.net/p/commons-collections |
| H | pg22808 | Maria João Magalhães | http://www.ohloh.net/p/cassandra |
| B | pg22811 | Guilherme Rodrigues | http://www.ohloh.net/p/hbase |
| H | pg22812 | Tiago Jorge | http://www.ohloh.net/p/cassandra |
| C | pg22815 | Nuno Carvalho | https://www.ohloh.net/p/log4j |
| F | pg22832 | Tiago Guimarães | http://www.ohloh.net/p/commons-io |
| C | pg22840 | Cristiano Sousa | https://www.ohloh.net/p/log4j |
| B | pg23205 | Daniel Murta | http://www.ohloh.net/p/hbase |
| F | pg23208 | José Pinheiro | http://www.ohloh.net/p/commons-io |
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: