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

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

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:

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.

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:

• R. Leino and P. Müller. Using the Spec# language, methodology, and tools to write bug-free programs. LNCS 6029, pages 91-139. Springer, 2009.
• W. Dietl and P. Müller. Universes: Lightweight Ownership for JML. Journal of Object Technology, 4(8):5-32, 2005.
• Code Contracts User Manual. Microsoft Corporation, September 3, 2010

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