Métodos Formais em Engenharia de Software

Mestrado de [Engenharia] Informática (2010/11)

Tópicos

Avisos

27 Jul - A notas finais estão publicadas em Funcionamento.

11 Jul - A notas à data da época normal estão publicadas em Funcionamento.

18 Jun - Teste de VFS terá lugar na 2a.fa. dia 20, às 15:00, na sala 0.02.

16 Jun - Deadline para entrega do relatório (hard): 23-Jun

16 Jun - Atenção ao facto de, para evitar conflito com as JOIN (28-30 Jun), a Milestone 3 (final) terá lugar numa sexta-feira, dia 1-Jul. O escalonamento das apresentações será anunciado no respectivo sumário.

14 Jun - As classificações do teste de CSI podem ser consultadas em Funcionamento.

16 Mar - Informa~se que, devido a um imprevisto de ordem pessoal, o Prof. LSB não poderá dar aula amanhã de manhã.

10 Mar - Informa~se que hoje de tarde só há a sessão às 17h00 (aulas de VFS só na próxima semana)

09 Mar - A alocação de projectos + tutorias de PI(II) serão anunciadas na sessão de amanhã (17h00).

23 Fev - A agenda e acetatos da milestone 2 estão no tópico do projecto.

10 Fev - A workshop de apresentação de propostas de projectos por parte dos parceiros industriais da UCE terá lugar dia 03-Mar, ver Sumários)

10 Fev - A Milestone PI(2) terá lugar dia 24-Fev de manhã; de tarde decorrerá a apresentação dos módulos do 2º semestre)

20 Jan - O dia 3-Fev será integralmente dedicado ao módulo CSI (aulas de revisões e preparação para o teste de 10-Fev)

4 Jan - As notas da primeira milestone de PI1 foram publicadas.

21 Dez - Já estão online os enunciados de mais um mini-projecto e um exercício de leitura de AMT.

14 Dez - Qualidade de dois projectos de MFES (2009/10) analisada na Open Code Clinic da SIG

02 Dez - No dia 16 de Dezembro não haverá sessão de CSI - todo o dia será dedicado a AMT (docente: Joost Visser)

29 Nov - As notas do teste de Alloy foram publicadas na secção AMT.

24 Nov - A primeira milestone do Projecto Integrado terá lugar dia 2-Dez.

28 Set - As aulas da edição corrente da UCE (2010/11) iniciaram-se a 30-Out, às 9h00, na sala DI 1.08 do Departamento de Informática.

29 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 (30%).
  • 1 mini-projecto sobre Model Checking (20%).
  • 1 mini-projecto sobre Qualidade de Software (15%).
  • 1 exercício de leitura sobre Linguagens de Modelação (20%).
  • 1 exercício de leitura sobre Behavioral Interface Specification Languages (15%).

Notas

Número Nome Alloy (0-20) MC (0-4) QS (0-3) LM (0-4) BISL (0-3) Final (0-20)
pg15989 João Melo 15 2.75 2.5 1.75 2.25 14
pg16305 Iago Abal 20 4 3 4 3 20
pg16490 Jorge Mendes 18 3.5 2.5 2.75 1.5 16
pg16875 André Costa 2 2.25 2.5 2.5 1.5 9
pg17297 Manuel Sousa 11.5 2.25 2.5 2.75 2 13
pg17311 Leonel Braga 9 2.5 2.5     8
pg17904 Ricardo Alves 11.5 3 3 3.5 2.75 16
pg18378 Rui Gonçalo 10 4 2.5 2.5 1.5 14
pg18385 Daniel Quinta 11 2.5 2.5     8
pg18391 Nuno Oliveira 12 3   2.5 1.25 10

Mini-projecto sobre Model Checking

O objectivo deste mini-projecto é desenvolver uma pequena aplicação para realizar bounded model-checking simbólico de fórmulas LTL sobre redes de Petri elementares usando Alloy. Dada uma descrição de uma rede de Petri (idealmente no formato PNML), uma fórmula LTL, e um tamanho máximo para os traços, a aplicação deverá produzir um modelo Alloy equivalente, com uma asserção que verifica a fórmula dada.

Este mini-projecto deverá ser realizado em grupos de 2 alunos. O prazo de entrega é 30 de Janeiro de 2011. Até esta data deverão submeter por email para o docente responsável:

  • O código fonte da aplicação desenvolvida.
  • Um pequeno relatório com a descrição da estratégia de tradução implementada (max 5 páginas).

Grupo Número Nome
1 pg16305 Iago Abal
pg18378 Rui Gonçalo
2 pg17311 Leonel Braga
pg18385 Daniel Quinta
3 pg17297 Manuel Sousa
pg16875 André Costa
4 pg16490 Jorge Mendes
5 pg17904 Ricardo Alves
pg18391 Nuno Oliveira
6 pg15989 João Melo

Exercício de leitura sobre Linguagens de Modelação

O objectivo deste exercício é estudar uma linguagem de modelação formal alternativa ao Alloy. A tabela seguinte indica qual a linguagem que cada aluno deverá estudar:

Número Nome Linguagem
pg15989 João Melo VDM
pg16305 Iago Abal UML+OCL
pg16490 Jorge Mendes Z
pg16875 André Costa B
pg17297 Manuel Sousa VDM
pg17311 Leonel Braga UML+OCL
pg17904 Ricardo Alves Z
pg18378 Rui Gonçalo B
pg18391 Nuno Oliveira VDM
pg18385 Daniel Quinta UML+OCL

Este exercício deverá ser realizado individualmente. O prazo de entrega é 30 de Janeiro de 2011. Até esta data deverão submeter por email para o docente responsável:

  • Uma breve descrição da linguagem e das ferramentas associadas e uma análise comparativa das suas vantagens / desvantagens relativamente ao Alloy (max 2 páginas).
  • Um modelo formal de uma agenda semelhante ao apresentado na página 23 do livro do Alloy.

Mini-projecto sobre Qualidade 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 na seguinte publicação:

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

Para efeitos de comparação, vamos restringir-nos a browsers open-source, tais como Firefox, Chromium, Camino, K-Meleon, etc. Prentende-se apenas uma análise do código fonte específico do browser, excluindo o layout engine. Este mini-projecto deverá ser realizado em grupos de 2 alunos. Cada grupo deverá analisar um browser 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 Janeiro de 2011. 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 essa performance.

Grupo Número Nome Browser
1 pg16305 Iago Abal Chromium
pg17904 Ricardo Alves
2 pg18378 Rui Gonçalo Firefox
pg17311 Leonel Braga
3 pg18385 Daniel Quinta Lynx
pg16490 Jorge Mendes
4 pg17297 Manuel Sousa Goona
pg16875 André Costa

Exercício de leitura sobre Behavioral Interface Specification Languages

O objectivo deste exercício é estudar alguns tópicos avançados sobre behavioral interface specification languages, em particular a questão da ownership. Após leitura da bibliografia recomendada, deverão responder às seguintes questões:

  • Porquê a necessidade de especificar ownership em behavioral interface specification languages tais como JML ou Spec#?
  • Qual a estratégia normalmente usada para essa especificação?
  • O framework Code Contracts não prescreve nenhum mecanismo para especificar ownership. Poderá ocorrer algum problema na verificação dos contractos e invariantes devido a essa ausência? Em caso afirmativo, ilustre a sua resposta com um exemplo onde esses problemas ocorrem.

Bibliografia recomendada:

Este exercício deverá ser realizado individualmente. O prazo de entrega é 30 de Janeiro de 2011. Até esta data deverão submeter as respostas por email para o docente responsável (max 2 páginas).

r20 - 26 Jul 2011 - 11:15:05 - AlcinoCunha
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM