Especificação e Modelação

2020/21

Programa

• Lógicas para especificação e modelação
  • Lógica de primeira ordem
  • Lógica relacional
  • Lógica temporal
• Técnicas de análise e verificação
  • Model-finding para lógica relacional
  • Model-checking para lógica temporal
• Linguagens e ferramentas
  • Alloy (Electrum) e o respectivo Analyzer
  • TLA+ e a respectiva Toolbox
  • SMV e NuSMV

Docente e Horário

Docente	Foto	Horário	Sala
Manuel Alcino Cunha		5a-feira, 9h-11h	CP1 1.21

Alunos

#	Nome	Curso	Grupo
a83916	Ana João Dias de Almeida	MiEI	5
a85516	António Manuel Carvalho Gonçalves	MiEI	9
a80453	Bárbara Andreia Cardoso Ferreira	MiEI
a82529	Carlos Manuel Marques Afonso	MiEI	3
a34900	Cecília da Conceição de Oliveira Soares	MiEI	13
a67683	César Eduardo da Silva Magalhães	MiEI	7
pg41842	César Hugo Moreira da Silva	MEI	12
a80970	Davide da Silva Matos	MiEI	15
a76089	Etienne da Silva Filipe Amado da Costa	MiEI	11
a85731	Gonçalo José Azevedo Esteves	MiEI	9
a86617	Gonçalo Pinto Nogueira	MiEI	3
a81283	Hugo Filipe Oliveira de Sousa Faria	MiEI	1
a85573	Jorge Gabriel Alves Cerqueira	MiEI	5
a84776	José Emanuel Silva Rodrigues	MiEI	2
pg42839	José Gonçalo Macedo Costa	MEI	7
a84577	José Pedro Oliveira Silva	MiEI	14
a85954	Luís Mário Macedo Ribeiro	MIEI	14
a71407	Maurício Zulueta Lima Salgado	MiEI	10
a85700	Pedro Miguel Araújo Costa	MiEI	10
a84783	Pedro Miguel Borges Rodrigues	MiEI	14
a86266	Rafael Inácio Lourenço	MiEI	2
a75411	Ricardo Guerra Leal	MiEI	15
a81716	Rodolfo António Vieira da Silva	MiEI	1
a80789	Rui Filipe Brito Azevedo	MiEI	11
pg36086	Vítor Hugo Gonçalves Silva	MMC	6

Método de avaliação

• 1 teste individual escrito (60%, ≥ 8)
• 1 trabalho a realizar em grupos de 2 alunos (20%)
• Avaliação contínua (20%)

Material Pedagógico

Acetatos

• Course presentation
• Electrum overview
• First-order logic
• Relational logic
• Type system
• Relational model finding
• First-order linear temporal logic
• Safety, liveness, and fairness
• Bounded model checking
• Computation tree logic
• CTL model checking
• LTL model checking

Exemplos

• Leader election in a ring (Electrum, TLA+)
• Distributed transactions (Electrum, TLA+)

Exercícios

• Alloy4Fun
  • Trash FOL
  • Classroom FOL
  • Trash RL
  • Classroom RL
  • Graphs
  • Labelled Transition Systems
  • CV Management
  • Production Lines
  • Trash TL
  • Trains TL
• Analyzer
  • Cards
  • Trains
  • Two-phase
  • Grandparent
• Desafios
  • http://alloy4fun.inesctec.pt/MuqgwjouPRQ4PWHw5
  • http://alloy4fun.inesctec.pt/3vW9wNnPqNDC4cb4u
  • http://alloy4fun.inesctec.pt/34dtAqKXoYoRfbN4Q
  • http://alloy4fun.inesctec.pt/3N5BoPYnHf2cFrwgv
  • Camaleões (solução)
  • Filósofos (solução)
• Modelos dos testes
  • Echo

Trabalho de grupo

O trabalho consiste em traduzir uma especificação feita em TLA+ para Electrum. Pode ser feito em grupos de até 3 elementos, mas espera-se que a extensão do trabalho realizado seja proporcional à dimensão do grupo. A entrega deverá ser feita por email até ao dia do teste (14 de Janeiro). O email deve explicar as principais opções tomadas e dificuldades sentidas, e incluir como anexo a especificação em Electrum, assim como o theme desenvolvido. Opcionalmente podem também fazer algumas comparações de performance entre as duas ferramentas.

Cada grupo deve optar por uma das seguintes especificações em TLA+. Agradeço que me informem logo que possível qual a constituição do grupo e especificação escolhida. No máximo cada especificação deverá ser trabalhada por 3 grupos, sendo a alocação de grupos a especificações publicada nesta página.

• Resource allocator Existem várias versões da especificação do allocator: uma abstracta (SimpleAllocator.tla), uma com escalonamento (SchedullingAllocator.tla), e uma especificação de uma implementação distribuída (AllocatorImplementation.tla). Em função da dimensão do grupo e objectivo de nota podem optar por traduzir apenas uma ou mais destas especificações.

Grupo	#1	#2	#3	Entrega
1	a81716	a81283		12 Jan
2	a86266	a84776		13 Jan
3	a86617	a82529		14 Jan

• Termination detection in a ring Especificação relativamente simples. Para notas mais altas ou grupos maiores podem também especificar esta variante.

Grupo	#1	#2	#3	Entrega
5	a83916	a85573		14 Jan
6	pg36086			14 Jan
7	a67683	pg42839		14 Jan

• Distributed mutual exclusion Especificação de um algoritmo distribuído de exclusão mútua.

Grupo	#1	#2	#3	Entrega
9	a85516	a85731		14 Jan
10	a85700	a71407		14 Jan
11	a76089	a80789		13 Jan
12	pg41842			13 Jan

• Paxos distributed algorithm Especificação do algoritmo distribuído Paxos para obter um consenso. Existem duas versões da especificação: uma muito abstracta (Voting.tla) que especifica a ideia de usar votações para obter o consenso, e uma especificação de alto nível do algoritmo (Paxos.tla). Em função da dimensão do grupo e objectivo de nota podem optar por traduzir apenas a primeira ou ambas as especificações.

Grupo	#1	#2	#3	Entrega
13	a34900			14 Jan
14	a85954	a84577	a84783	13 Jan
15	a75411	a80970		18 Jan

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.
• L. Lamport. Specifying Systems: the TLA+ language and tools for hardware and software engineers. Addison-Wesley, 2002.

Outras leituras recomendadas

• D. Jackson. Alloy: a language and tool for exploring software designs. Commun. ACM 62(9): 66-76 (2019). Também existe um vídeo sobre este artigo que pode ser visto aqui.
• Leslie Lamport. If You’re Not Writing a Program, Don’t Use a Programming Language. Bulletin of the EATCS 125 (2018)
• Jonathan Edwards, Daniel Jackson, Emina Torlak. A type system for object models. SIGSOFT FSE: 189-199 (2004)
• Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu. Symbolic Model Checking without BDDs. TACAS: 193-207 (1999)
• Alcino Cunha. An Overview of Electrum. 2020.
• Alcino Cunha. Structural Design with Alloy. 2020.
• Leslie Lamport. A summary of TLA+. 2000.

Ferramentas

• Electrum (a última versão pode ser encontrada aqui)
• Alloy
• NuSMV
• TLA+