Métodos Formais em Engenharia de Software

Mestrado Integrado em Engenharia Informática - MFES 2018/2019

Tópicos

Avisos

16 Jan - CSI: tinynew.gif o teste de CSI de amanhã decorrerá na sala 0.05 do DI.

15 Jan - EM: as notas do segundo teste foram lançadas no blackboard da disciplina. tinynew.gif

11 Jan - CSI: as notas do mini-teste foram lançadas na página de CSI.

9 Jan - EM: o teste de EM decorrerá na sala 0.05 do DI.

30 Dec - EM: as notas do TP1 e do primeiro mini-teste foram lançadas no blackboard da disciplina.

21 Dec - EM: foi lançado o enunciado do TP2 sobre Alloy na página EM. A data limite da entrega é 20-Jan.

13 Dez - O segundo teste de EM decorrerá no dia 10-Jan às 9h00 (sala a indicar). O segundo teste de CSI decorrerá no dia 17-Jan (sala e hora a confirmar).

8 Dez - Lista recente e actualizada de empresas que usam métodos formais na indústria.

28 Nov - CSI: haverá hoje uma aula de dúvidas às 16h00, na sala 1.16.

24 Nov - CSI: já está disponível o formulário na página de CSI, bem como algumas FAQs.

24 Nov - CSI: o mini-teste decorrerá às 14h00 de 29-Nov, na sala das aulas. Os alunos podem consultar (apenas) informação escrita ou impressa.

14 Nov - EM: o primeiro teste decorrerá às 9h00 na sala das aulas. Podem usar os portáteis para testar execuções no NuSMV.

8 Nov - CSI: em casa, completar os invariantes I3 e I4 do modelo Alloy do problema Plano de Estudos do MEI saído da aula de hoje material pedagógico na página CSI.

5 Nov - CSI: há novo material pedagógico na página CSI.

25 Out - EM: foi lançado o enunciado do TP1 sobre NuSMV na página EM. A data limite da entrega é 11-Nov.

21 Out - CSI: ver exemplos Alloy das aulas na página CSI.

02 Out - CSI: preparação para as aulas: ver tinynew.gif sumários previstos e seguir as respectivas indicações nos apontamentos fornecidos na bibliografia. (Em CSI segue-se o método 'Flipped Classroom')

15 Set - Início das aulas: 20-Set, 9h00, sala E7 1.10.

Education » MFES » WebHome » EM

Especificação e Modelação

Docente / Horário

Docente Foto Horário Sala
Nuno Moreira Macedo nm 5a-feira, 9h-12h Sala E7 1.10

NB: poderá haver trocas de horário entre EM e CSI de acordo com necessidades de serviço dos docentes das duas disciplinas.

Alunos

Afonso Rafael Carvalho Sousa A74196 MiEI
Alexandre Miguel Costa Dias A78425 MiEI
Armando João Isaias Ferreira dos Santos A77628 MiEI
Artur Queiroz PG38014 MMC
Diogo Manuel Macedo e Silva A79021 MiEI
Francisco Fernando Vilela Araújo A79821 MiEI
Fábio Rafael Pereira Araújo A78508 MiEI
Gerson Benjamim Hungulu PG35957 MMC
Gonçalo Medeiros São Pedro Raposo A77211 MiEI
Gonçalo Nuno Esteves Duarte A77508 MiEI
Joana Fernandes Cunha PG38929 MEI
Jorge Fernando Alves da Cruz A78895 MiEI
José Carlos do Vale e Sousa A74678 MiEI
João Manuel da Silva Gomes Fernandes PG38930 MEI
Nelson Loureiro PG37020 MMC
Patrícia Filipa Bouça Barreira A79007 MiEI
Pedro Faria Durães da Silva A78434 MiEI
Pedro Henrique Moreira Gomes Fernandes A77377 MiEI
Pedro Miguel Silva PG38935 MEI
Ricardo Guerra Leal A75411 MiEI
Tiago André Araújo Monteiro A78961 MiEI

Método de avaliação

  • 2 testes individuais escritos (70%, ≥ 8).
  • 2 trabalhos de grupo (30%, ≥ 10)

Notas

  • Lançadas no blackboard da disciplina (TP1 e 1º mini-teste).

Enunciado do Trabalho 1 sobre NuSMV

O Sistema Europeu de Gestão de Tráfego Ferroviário (ERTMS, European Rail Traffic Management System) é um conjunto de padrões que visa garantir a interoperabilidade de linhas ferroviárias na União Europeia. O seu componente de sinalização e controlo, o Sistema Europeu de Controlo de Comboios (ETCS, European Train Control System), estabelece vários níveis de conformidade com o padrão, dependendo do nível de tecnologia já implementado nas linhas e nos comboios. O Nível 3 assume que os comboios estão em comunicação constante com o sistema de controlo, a transmitir informação sobre a sua posição e integridade. Visto na prática estes sistemas ainda não serem totalmente viáveis, o Nível 3 Híbrido assume ainda a existência de sensores físicos na linha que detectam a presença de carruagens, e permitem colmatar falhas nos sistemas de deteção e comunicação.

O objetivo deste trabalho é modelar, especificar e verificar, em NuSMV, parte do conceito Nível 3 Híbrido do ERTMS/ETCS. Para tal devem basear-se no seguinte documento introdutório, assim como na especificação completa, nomeadamente na máquina de estados presente na Secção 5 e nos cenários operacionais do Anexo A. As componentes do conceito a modelar, assim como o nível de detalhe, ficam ao critério de cada grupo. Para simplificar o processo, o modelo deve representar apenas uma configuração da linha, no máximo tão complexa quanto a dos cenários operacionais do Anexo A do documento (9 blocos virtuais).

Os grupos (de 2 elementos) deverão entregar por email o trabalho até à data limite de 11-Nov-2018 (um ficheiro zip com todos os modelos desenvolvidos, devidamente comentados).

Enunciado do Trabalho 2 sobre Alloy

Uma tabelas de hash distribuída (DHT) é um sistema distribuído descentralizado que disponibiliza as funcionalidades de uma tabela de hash. Pares (chave, valor) estão distribuídos pelos vários nós, e o algoritmo de lookup garante que o valor associado a uma chave pode ser encontrado eficientemente. Para tal, algumas DHT organizam os nós numa estrutura em anel em que o identificador atribuído a cada nó orienta a pesquisa. No entanto, isto requer que a rede inevitavelmente estabilize num anel quando nós entram ou abandonam a rede. Um desses protocolos é o Chord, que foi previamente validado em Alloy. Outra alternativa é o Pastry, que foi validado previamente em TLA+, uma outra linguagem de especificação com um model checker associado.

Os grupos de trabalho devem estudar o artigo sobre a análise do Pastry 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 TLA+, mas apenas na medida do que é necessário para perceberem o artigo. O que se pretende neste trabalho é analisar o Pastry usando Alloy em vez de TLA+. Se necessário, mas não obrigatoriamente, podem usar a especificação do Chord em Alloy como inspiração. O nível de detalhe a atingir, assim como a escolha do idioma de Alloy dinâmico, fica à consideração de cada grupo. Finalmente, os grupos devem também desenvolver um theme que facilite a compreensão das instâncias.

Os grupos deveram entregar por email o trabalho até à data limite de 20-Jan-2018 (um modelo Alloy, devidamente comentado, e o respectivo theme).

Material pedagógico

Parte 1 - NuSMV

Parte 2 - Alloy

Bibliografia

Ferramentas

r31 - 10 Jan 2019 - 20:08:59 - NunoMacedo
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM