Métodos Formais em Engenharia de Software

Mestrado de [Engenharia] Informática (2012/13)

Tópicos

Avisos

15 Jul - Exame de recurso do módulo CSI - terá lugar dia tinynew.gif 18 de Julho (5ª-feira), às 9h30, na sala DI 1.08.

15 Jul - Publicadas as notas finais da época normal em tinynew.gif Funcionamento

6 Jul - As notas finais de AMT foram publicadas.

10 Jun - As classificações do teste de CSI encontram-se em Funcionamento.

08 Jun - Milestone 4 (PI): recomenda-se a leitura de How to write a great research paper (ver tinynew.gif Projecto) na preparação dos slides+relatório a apresentar nesta milestone final.

06 Jun - A Milestone 4 do PI terá lugar no dia 27-Jun - ver planeamento em tinynew.gif Sumários.

06 Jun - Chama-se a atenção dos alunos para o preenchimento na intranet dos inquéritos pedagógicos até tinynew.gif 3-Jul 2013.

13 Fev - Teste do módulo CSI - terá lugar dia 1 de Março (6ª-feira), às 9h00, na sala DI 1.08.

04 Jan - a milestone nr.1 do Projecto integrado terá lugar na próxima quinta-feira, 10-Jan, das 14h00 às 18h00, na sala DI 1.08 (1º andar do edifício do DI), sendo transmitidas via Skype para os supervisores nas empresas.

13 Nov - A WS de apresentação dos projectos (PI) aos alunos aulas terá lugar na próxima quinta-feira, 15-Nov, das 12h00 às 18h00, na sala DI 1.08 (1º andar do edifício do DI).

28 Set - As aulas iniciam-se na próxima quinta-feira, 4-Out, às 9h00, na sala DI 1.08 (1º andar do edifício do DI).

24 Set - A apresentaçao desta UC na Semana Inaugural MEI @ 2012/2013 terá lugar no dia 27-Set às 16h00, ver Sumários.

13 Set - Criação do site.

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:

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
A pg22796 André Santos http://www.ohloh.net/p/commons-collections
pg21319 Victor Miraldo
B pg23205 Daniel Murta http://www.ohloh.net/p/hbase
pg22811 Guilherme Rodrigues
C pg22840 Cristiano Sousa https://www.ohloh.net/p/log4j
pg22815 Nuno Carvalho
E pg22576 Tiago Ferreira http://www.ohloh.net/p/wicket
pg22577 Xavier Pinho
F pg22832 Tiago Guimarães http://www.ohloh.net/p/commons-io
pg23208 José Pinheiro
G   Thiago Ramos http://www.ohloh.net/p/jackrabbit-oak
  Deise Santana Maia
H pg22812 Tiago Jorge http://www.ohloh.net/p/cassandra
pg22808 Maria João Magalhães
pg16334 José Miguel Magalhães

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:

r19 - 06 Jul 2013 - 11:32:49 - AlcinoCunha
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM