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

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.

Equipa docente

Luís Soares Barbosa
José Bernardo Barros
Manuel Alcino Cunha
Maria João Frade (*)
José Nuno Oliveira
Jorge Sousa Pinto

(*) Em licença sabática no corrente ano lectivo.

Docentes convidados

Joost Visser (SIG)

Índice do material disponível:

Bibliografia

• Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen, Jiri Srba. Reactive Systems: Modelling, Specification and Verification. CUP, 2007.

• Christel Baier, Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008.

• Daniel Jackson. Software abstractions: logic, language, and analysis. MIT Press, 2006.

• C.B. Jones. Systematic Software Development Using VDM. Series in Computer Science. Prentice-Hall International, 1986 (first edition). (345 pages)

• Robin Milner. Communicating and Mobile Systems: The Pi Calculus. CUP, 1999.

• J.N. Oliveira. Transforming Data by Calculation. In volume 5235 of LNCS, pages 134-192, 2008.

• J.N. Oliveira. Extended static checking by calculation using the pointfree transform. In A. Bove et al., editor, volume 5520 of LNCS, pages 195-251. Springer-Verlag, 2009.

• Pitts A. M. Lecture Notes on Semantics of Programming Languages. Univ Cambridge, 1997-2002 (disponível online aqui)

Divulgação

• Daniel Jackson. Dependable Software by Design. Scientific American, Junho 2006.

• Daniel Jackson. A Direct Path to Dependable Software. DOI:10.1145/1498765.1498787, Abril 2009.

• David Parnas. Really Rethinking 'Formal Methods'. IEEE Computer 43(1), 28–34 (2010).

Acetatos

• J.N. Oliveira. Data type invariants: starting where (static) type checking stops (24 slides)

• J.N. Oliveira. Pre / post-conditions -- starting where (pure) functions stop (29 slides)

• J.N. Oliveira. PF transform: when everything becomes a relation (43 slides)

• Alcino Cunha. An introduction to Alloy. Versão definitiva.

• J.N. Oliveira. PF transform: conditions and coreflexives for ESC (28 slides)

• J.N. Oliveira. “Theorems for free”: a (calculational) introduction (27 slides)

• J.N. Oliveira. PF-transform: using Galois connections to structure relational algebra (35 slides)

• Alcino Cunha. A perspective on model-checking.

• Joost Visser. Software Analysis and Testing (parte 1, parte 2, parte 3, parte 4).

• Luís S. Barbosa. Labelled transition systems (revised notes, 2011.04.02).

• Luís S. Barbosa. Introduction to CCS.

• Luís S. Barbosa. Hennessy-Milner logic.

• Luís S. Barbosa. The modal mu-calculus.

• Luís S. Barbosa. Introduction to mCRL2 (and mini-project).

• Luís S. Barbosa. An introduction to Reo.

Exemplos

• Alloy: eu sou o meu próprio avô, sistema de ficheiros, e barqueiro.

• Alloy: noDuplicates.zip

Exercícios

• Colectânea de exercícios de testes sobre Alloy.

• Exercícios sobre lógica temporal e model-checking.

• J.N. Oliveira. (2010.11.07) CSI Module — List of classroom exercises

(23 exercises)

• Formulário do Cálculo Relacional (7 págs)

• Luís S. Barbosa. Exercises on labelled transition systems.

• Luís S. Barbosa. Exercises on CCS.

Software

• Alloy Analyzer
• Uppaal
• Coq
• Frama-C
• VDM/Overture

Repositórios

• Repositório de ferramentas da associação FME.

Enunciados de provas de avaliação individual

• Módulo CSI (10-Fev): enunciado.
• Módulo CSI (21-Jul): enunciado .
• Módulo VFS (20-Jun): enunciado.
• Módulo VFS (21-Jul): enunciado.

Projecto Integrado (II)

Gr	Nome	Nr	Fotografia	Tema
Grupo Critical Software
1	João Silva de Melo	pg15989		ANÁLISE DA PROPAGAÇÃO DE FALHAS EM SISTEMAS COMPLEXOS
Grupo Galois
2a	Iago Abal Rivas	pg16305		Using quantified rewrite patterns with SMT solvers
2b	Jorge Cunha Mendes	pg16490		High Assurance Digitial Signal Processing
	Paul van der Walt	E4083
Grupo Brazilian Aeronautics and Space Institute
3	Daniel Ribeiro Quinta	pg18385		Safety Critical Interactive Computing Systems’ Modelling
	Manuel António Freitas de Sousa	pg17297
Grupo Primavera Software Factory
4	Leonel João Fernandes Braga	pg17311		Verificação formal de um componente de cálculo do IVA
	Rui Miguel de Carvalho Gonçalo	pg18378
Grupo Software Improvement Group
5	André Vilas Boas da Costa	pg16875		Analysis of OSS projects
	Ricardo Daniel Queirós Alves	pg17904

Projecto Integrado (I)

Milestone 1

• Objectivos:
  • Especificar em Alloy um problema de média dimensão.

• Deadline:
  • 28 de Novembro de 2010.

• Deliverables:
  • Modelo Alloy (25%).
  • Apresentação de 20m no dia 2 de Dezembro de 2010 (10%).
  • Arguição da apresentação de outro grupo (5%).

Milestone 2

• Objectivos:
  • Implementar um protótipo do sistema modelado na Milestone 1 segundo a filosofia DbC.
  • Efectuar teste do código por forma a atingir uma cobertura aceitável.
  • Recolher métricas com o objectivo de avaliar a qualidade

• Deadline:
  • 20 de Fevereiro de 2011.

• Deliverables:
  • Código, testes e métricas (25%).
  • Apresentação de 20m no dia 24 de Fevereiro de 2011 (10%).
  • Arguição da apresentação de outro grupo (5%).
  • Relatório do trabalho desenvolvido em PI1 (20%).

Relatório

O relatório de PI1 deverá ter 15 páginas no máximo, excluindo anexos, e seguir o template LaTeX apresentado abaixo. Sugere-se a seguinte estruturação de secções:

• Introdução: descrição do problema; descrição informal dos objectivos de verificação; breve apresentação das linguagens / ferramentas a usar na implementação; breve apresentação da estrutura do relatório.
• Modelo Alloy: apresentação das assinaturas e operações mais relevantes, justificando as opções tomadas; enumeração dos invariantes, factos e asserções mais relevantes; resultados da verificação.
• Implementação: descrição da metodologia usada para refinar o modelo para código; apresentação dos contratos e invariantes mais relevantes.
• Teste e Qualidade do Código: descrição da metodologia de testes utilizada; análise da cobertura dos mesmos; descrição das métricas utilizadas e avaliação da qualidade do código fonte.
• Conclusões: sintetizar os resultados positivos e negativos mais relevantes; avaliação crítica das linguagens e ferramentas utilizadas (incluindo sugestões de melhoria); breve comparação com outras formalizações do mesmo problema.

\documentclass[a4paper]{article}

\usepackage[portuges]{babel}
\usepackage[latin1]{inputenc}
\usepackage{a4wide}

\begin{document}

\end{document}

.natBreadCrumbs { width:0px; height:0px; overflow:hidden; }

.avisos { color: #444; font-size:12px; }

.natWebTitle { font-size:25px; }

.natMainFooterContents, .natMainHeaderContents { padding:0px; margin:0px 0px; }

See also the faster WebTopicList

• TWikiGuest - example@your.company

Web Changes Notification Service

Each TWiki web has an automatic e-mail notification service that sends you an e-mail with links to all of the topics modified since the last alert.

Users subscribe to email notifications using their WikiName or an alternative email address, and can specify the webs/topics they wish to track using one of these bullet list formats:

three spaces * [ webname . ] wikiName - SMTP mail address
three spaces * [ webName . ] wikiName
three spaces * SMTP mail address
three spaces * SMTP mail address : topics
three spaces * [ webname . ] wikiName : topics

In the above examples, topics is a space-separated list of topic names. The user may further customize the specific content they will receive using the following formats:

• Specify topics without a Web. prefix
• Topics must exist in this web.
• Topics may be specified using * wildcards
• Each topic may optionally be preceded by a '+' or '-' sign. The '+' sign means "subscribe to this topic" (the same as not putting anything). The '-' sign means "unsubscribe" or "don't send notifications regarding this topic". This allows users to elect to filter out certain topics (and their children, to an arbitrary depth). Topic filters ('-') take precedence over topic includes ('+').
• Each topic may optionally be followed by an integer in parentheses, indicating the depth of the tree of children below that topic. Changes in all these children will be detected and reported along with changes to the topic itself. Note This uses the TWiki "Topic parent" feature.
• Each topic may optionally be immediately followed by an exclamation mark ! or a question mark ? with no intervening spaces, indicating that the topic (and children if there is a tree depth specifier as well) should be mailed out as complete topics instead of change summaries. ! causes the topic to be mailed every time even if there have been no changes, ? will mail the topic only if there have been changes to it. This only makes sense for subscriptions.

For example: Subscribe Daisy to all changes to topics in this web.

   * daisy.cutter@flowers.com

   * daisy.cutter@flowers.com: Web*

   * TWiki.DaisyCutter: Petal* (1) TWiki.WeedKillers (3) Pretty*Flowers

   * TWiki.StarTrekFan: Star* - *Wars - *sInTheirEyes - *shipTroopers

   * daisy@flowers.com: TWiki.NewsLetter?

   * buttercup@flowers.com: TWiki.NewsLetter! (1)

   * TWiki.GardenGroup: TWiki.AllNewsLetters? (3)
   * petunia@flowers.com: - TWiki.ManureNewsLetter

If a TWiki group is listed for notification, the group will be recursively expanded to the e-mail addresses of all members.

Tip: List names in alphabetical order to make it easier to find the names.

Note for System Administrators: Notification is supported by an add-on to the TWiki kernel called the MailerContrib. See the MailerContrib topic for details of how to set up this service.

Note: If you prefer a news feed, point your reader to WebRss (for RSS 1.0 feeds) or WebAtom (for ATOM 1.0 feeds). Learn more at WebRssBase and WebAtomBase, respectively.

Related topics: WebChangesAlert, TWikiUsers, TWikiRegistration

Warning

Can't INCLUDE TWiki.WebSearchAdvanced repeatedly, topic is already included.

Statistics for Education/MFES1011 Web