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

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

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.

Grupo Número Nomedown Projecto
D pg25340 Yoan Ribeiro http://www.ohloh.net/p/Hadoop
F pg25301 Vitor Pereira http://www.ohloh.net/p/Apache-Commons-Math
H pg25263 Telma Correia http://www.ohloh.net/p/tomee
A pg25318 Rogério Pontes http://www.ohloh.net/p/apache-isis
E pg25332 Paulo Silva http://www.ohloh.net/p/xerces2-j
A pg25313 Nuno Laranjo http://www.ohloh.net/p/apache-isis
C   Miguel Costa http://www.ohloh.net/p/droids
F pg25311 Luís Romano http://www.ohloh.net/p/Apache-Commons-Math
G pg26133 João Carlos Alves Cruz http://www.ohloh.net/p/tomcat
E pg25285 Jorge Lobo http://www.ohloh.net/p/xerces2-j
G pg25299 Helder Afonso http://www.ohloh.net/p/tomcat
C pg22766 Fábio Esteves http://www.ohloh.net/p/droids
H pg26119 Fábio Fernandes http://www.ohloh.net/p/tomee
D pg25300 Damien Vaz http://www.ohloh.net/p/Hadoop
B pg19643 Catarina Correia http://www.ohloh.net/p/CloudStack
B pg25335 Ana Carvalho http://www.ohloh.net/p/CloudStack