Especificação e Modelação
Docente / Horário
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
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
