Métodos Formais em Engenharia de Software

Mestrado Integrado em Engenharia Informática [16/17]

Tópicos

Avisos

04 Set - Lançadas a classificações do exame da época especial de E&M .

15 Jul - Exames da época especial: ver Sumários.

22 Jun Notas dos testes e do TP2 já sairam - A&C.

06 Jun Nova data para apresentações dos trabalhos - 20 Junho, ver Sumários.

24 Mai Datas para entrega e apresentações dos trabalhos adiada - para 15 e 16 Junho, respectivamente.

9 Mai Anunciadas datas para as apresentações dos trabalhos (1 Junho) e para o teste (8 Junho).

9 Mai Disponíveis os slides mostrados até ao momento no último módulo de A&C.

25 Abr Entrega do trabalho prático (UPPAAL) adiado para 3 Maio @ 23:59.

6 Abr Notas do trabalho prático 1 já estão disponíveis - A&C.

20 Mar Trabalho prático 1: entregar até dia 23 Março; Trabalho prático 2: disponível em Material - A&C.

24 Fev - Primeiro trabalho prático já saiu, em "Material" de A&C.

14 Fev - Ver Material em A&C.

10 Fev - Lançadas a classificações finais de E&M.

10 Fev - Importante: as aulas das disciplinas do perfil de MFES passam, a partir da próxima semana (inclusive), para a sala DI 1.08.

6 Fev - WS de apresentação de temas MFES/LEI: ver Sumários.

6 Fev - Apresentações dos trabalhos: ver Sumários. Cada apresentação não pode demorar mais que 20 min, discussão incluída. No caso de desejarem apresentar slides devem enviá-los para o responsável da disciplina no dia anterior.

28 Jan - Trabalho de E&M: a data de entrega passou para 3-Fev até às 12h.

21 Jan - Enunciado do teste de E&M disponível, com correcção de algumas perguntas.

15 Jan - Estão disponíveis duas bolsas para desenvolver trabalho no projeto Green Software Laboratory GSL. Se tens licenciatura (ou os 3 primeiros anos do mestrado) completos concorre! Mais informações aqui.

06 Dez - E&M, T+TP suplementar de amanhã: por falta de salas a aula só poderá ser às 16h00, na sala 1.09, ver Sumários.

30 Nov - E&M: já está disponível o enunciado do TP.

29 Nov - ATS, aula extra esta 4a feira, dia 30/11 às 14:00.

29 Nov - E&M, grupos de trabalho: os alunos que ainda o não fizeram devem enviar ao responsável da disciplina a constituição do seu grupo (de dois alunos cada). O TP será anunciado amanhã, 30-Nov.

20 Nov - E&M, preparação em casa para a próxima aula ('Flipped Classroom'): ler slides (PDF) até ao 115; fazer os exercícios 37, 40, 46 e 47.

3 Nov - Está disponível uma bolsa para desenvolver trabalho na plataforma Alloy4Fun. Se tens licenciatura (ou os 3 primeiros anos do mestrado) completos concorre! Mais informações aqui.

13 Out - E&M, preparação em casa para a próxima aula ('Flipped Classroom'): ler slides até ao 97; fazer os exercícios 32, 33, 34.

3 Out - E&M, preparação em casa para a próxima aula ('Flipped Classroom'): ler slides até ao 79; fazer os exercícios 25, 28, 30, 31.

29 Out - E&M, preparação em casa para a próxima aula ('Flipped Classroom'): ler slides até ao 65; fazer os exercícios 20, 22, 25-26.

14 Out - E&M, preparação em casa para a próxima aula ('Flipped Classroom'): ler slides até ao 45; fazer os exercícios 7 a 10.

6 Out - O teste de ATS será no dia 5 de Janeiro e o teste de E&M será no dia 12 de Janeiro.

20 Set - As aulas das disciplinas do primeiro semestre iniciam-se a 22-Set.

Especificação e Modelação

Classificações do exame da época especial:

a64287 = R; pg22842 = R.

Classificações finais:

(Apenas dos alunos avaliados):

a32652 = 10; a53791 = 10; a64287 = R; a64365 = R; a67652 = F; a67709 = 10; a70058 = F; a70430 = 14; a70441 = 10; a70644 = F; a71580 = 13; a71625 = F; a72204 = 11; a72205 = R; a72227 = 11; a72424 = 14; pg22842 = F; pg31577 = 10; pg32996 = R.

Método de avaliação

  • Teste individual escrito (70%, ≥ 8)
  • Trabalho de grupo (30%, ≥ 10)
  • Presença obrigatória nas aulas

Enunciados de provas escritas de avaliação (T)

Data Descrição Ficheiro
12-Jan-2017 Teste PDF (com a tinynew.gif correcção de algumas perguntas)
26-Jan-2017 Exame de recurso PDF

Enunciado do Trabalho (TP)

Introdução - Nesta disciplina foram estudados métodos de especificação, modelação e raciocínio para a produção de software de alta fiabilidade. Todos os sistemas de segurança-crítica exigem software fiável, por exemplo nos equipamentos médicos, nos transportes aéreos, etc. A norma de certificação DO-178B é uma diretriz sobre segurança do software crítico destinado à aviação.

O artigo Modelling an Aircraft Landing System in Event-B, que descreve a modelação formal de um sistema de controlo do trem de aterragem de um avião baseado nos requisitos impostos pela Federal Aviation Administration dos EUA, é o ponto de partida para este trabalho.

O que é para fazer - os grupos de trabalho devem estudar o artigo acima referido com atenção por forma a perceberem bem qual é o problema que é abordado. Ao mesmo tempo, deverão informar-se sobre a linguagem de modelação Event-B, mas apenas na medida do que é necessário para perceberem o artigo. O que se pretende neste trabalho é exprimir o mesmo modelo em Alloy, de forma o mais simples possível. Note-se que não se pretende uma tradução à letra do modelo dado, mas antes um modelo independente e simplificado. Mais do que a quantidade, valorizar-se-á a qualidade e a capacidade de abstracção.

Prazos e "deliverables" - os grupos deveram entregar, até à data limite de 31-Jan-2017, um pequeno relatório (em inglês) onde conste o código Alloy que desenvolveram. Deverão também preparar uma apresentação do seu trabalho (slides) prevista para (no máximo) 10 minutos. As orais destas apresentações decorrerão de 1 a 10 de Fevereiro.

Os alunos deverão estar atentos a esta página quanto a prováveis esclarecimentos sobre este trabalho que os inicia na aplicação de métodos formais a problemas reais. Bom trabalho!

Material pedagógico

Bibliografia

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

Ferramentas

Exemplos / bibliotecas Alloy

  • Módulo Alloy: RelCalc.als - Cálculo relacional básico em Alloy.

Desafios Alloy

Alunos

Nome P/C Nr Curso Grupo Fot
Axel da Silva Ferreira C a53064 MiEI G4 A53064
Daniel Gonçalves Rodrigues C a67634 MiEI G9 a67634
Daniel da Fonte Torres EC a70058 LCC G8 a70058
David António Cardoso Moreira P a64287 MiEI G2 a70058
David Miguel Duarte Rodrigues Alves C a53791 MiEI (cong) A53791
Diana Filipa Oliveira C a67652 MiEI G7 a67652
Diogo Filipe da Silva Vilaça P a72227 MiEI G3 A72227
Fernanda Raquel Cerdeira Alves C a64365 MiEI G2 a64365
Fátima Cristiana da Costa Conceição P pg22842 MMC (cong) pg22842
Gil Gonçalves C a67738 MiEI G7 a67738
Hugo Filipe da Silva Ribeiro P pg32996 MEI G5 pg32996
Isac Pereira Oliveira Meira P pg31577 MEI G8 pg31577
José Nuno Castro de Macedo P a72424 MiEI G3 A72424
José Paulo Queiroga Amorim Fernandes P a72204 MiEI G6 a72204
João Bernardo Machado Quintas Dias da Costa P a70430 MiEI G1 A70430
João Luís Braga Simões Romero C pg31384 MEI G5 pg31384
Luís Martinho de Aragão Rego da Silva C a72205 MiEI G9 a72205
Mário Jorge Viana Ferreira P a70441 MiEI G6 a70441
Nelson Arieira Parente C a71625 MiEI
Nuno Alberto Pires Fernandes C a61066 MiEI G4 A61066
Pedro Duarte Cardoso Lopes C a32652 MiEI (cong) A32652
Rafael Alexandre Antunes Barbosa P a71580 MiEI G1 A71580
Ruben Miguel Cunha Santos C a70644 MiEI
Saulo Rodrigues e Silva ? id5541 PDINF
Sandra Isabel Lopes Ferreira P a67709 MiEI (cong) a67709

Atendimento electrónico (FAQs) tinynew.gif

(Esta secção será actualizada regularmente com as dúvidas mais frequentes que forem colocadas à equipa docente.)

  • Q1 - Tenho dificuldade em decorar a diferença entre núcleo e imagem de uma relação. Há alguma mnemónica que possa ajudar?

R: Haverá concerteza muitas, por exemplo: decore o nome feminino "NEIDE" e leia-o como o acrónimo de "Núcleo, Esquerda, Imagem, Direita, Etc", isto abreviatura de "num núcleo Rº.R o converso está à esqerda, numa imagem R.Rº está à direita, etc". Haverá melhores, mas este já pode ajudar.


  • Q2 - Se eu tiver <∀ a,b : a X b : a=b> posso trocar para <∀ a,b : a=b : aXb> e depois aplicar 'one point', correcto?

R: Não (!) Isso é se o quantificador for o existencial (∃). No caso do universal, a troca possível é de <∀ a,b : a X b : a=b> para <∀ a,b :: a X b => a=b>, cf. a regra Trading (∀) dos slides, para R = true.


r40 - 04 Sep 2017 - 10:19:09 - JoseNunoOliveira
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM