Especificação e Modelação

Docente / Horário

Docente	Foto	Horário	Sala
Nuno Moreira Macedo		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

Método de avaliação

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

Notas

• Lançadas no blackboard da disciplina (TPs e testes).
• Correção parcial do 1º teste.
• Correção parcial do 2º 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

• Modeling, Specification (and Verification): slides introdutórios.
• NuSMV: slides de introdução ao NuSMV (modelação, simulação, especificação, verificação).
• NuSMV 2.6 User Manual.
• Exercícios SMV: ficha de exercícios sobre SMV.
• Exemplos SMV: cadeira.smv, farmer.smv, peterson_nomodules.smv, peterson_modules.smv.
• Model Checking: slides de introdução ao model checking.

Parte 2 - Alloy

• Exercícios de revisão de lógica de primeira-ordem tipada.
• Exercícios sobre lógica relacional tipada com fecho transitivo.
• Alloy: slides de introdução ao Alloy.
• Desafios sobre invariantes estruturais em Alloy:
  • Agenda telefónica.
  • Leilões.
  • Unidades curriculares.
  • Alocação de memória.
  • Hierarquia Java.
  • Revisão científica.
  • Linhas de produção.
  • Plataforma de currículos.
• Exemplo ERTMS Alloy, versão estática e theme.
• Exemplo agenda eletrónica Alloy, versão idioma de eventos.
• Safety & liveness in Alloy: slides de introdução à modelação dinâmica em Alloy.
• Exercícios Alloy: ficha de exercícios sobre Alloy (incluindo dinâmicos).
• Exemplo ERTMS Alloy, versões dinâmicas, verificação direta e indireta, e theme.
• Alloy: Under the Hood: breve apresentação da semântica, sistema de tipos, e arquitectura de verificação do Alloy.

Bibliografia

• C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.
• D. Jackson. Software abstractions: logic, language, and analysis. Revised edition, MIT Press, 2012.

Ferramentas

• NuSMV
• Alloy