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.

Projecto Integrado (II)

Grupos, alunos e temas.

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

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

Grupo Número Nome Projecto Nota
Grupo 1 pg16490 Jorge Mendes LDAP 7.25
pg18391 Nuno Oliveira 7.25
Grupo 2 pg17311 Leonel Braga NAnt 5.25
pg18378 Rui Gonçalo 5.75
  Daniel Quinta 5.25
Grupo 3 pg16305 Iago Abal Darcs 7.75
pg15989 João Melo 7.5
Grupo 4 pg17904 Ricardo Alves SGBD 5.75
pg16875 André Costa 5.5
pg17297 Manuel Sousa 5.25

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

Grupo Número Nome Projecto Apresentação Arguente Nota
Grupo 1 pg16490 Jorge Mendes LDAP 10:00 Grupo 2 9
Grupo 2 pg17311 Leonel Braga NAnt 10:30 Grupo 3 9.5
Grupo 2 pg18378 Rui Gonçalo NAnt 10:30 Grupo 3 9.5
Grupo 2   Daniel Quinta NAnt 10:30 Grupo 3 9.5
Grupo 3 pg16305 Iago Abal Darcs 11:00 Grupo 4 11.75
Grupo 4 pg17904 Ricardo Alves SGBD 11:30 Grupo 5 9
Grupo 4 pg16875 André Costa SGBD 11:30 Grupo 5 9
Grupo 4 pg17297 Manuel Sousa SGBD 11:30 Grupo 5 9
Grupo 5 pg15989 João Melo Darcs 12:00 Grupo 1 7.5

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}

r19 - 14 Jun 2011 - 17:04:12 - JoseNunoOliveira
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM