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).
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:
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.