Especificação e Modelação
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
- Simulação
- Model-finding para lógica relacional
- Model-checking para lógica temporal
- Linguagens e ferramentas principais
- Alloy e o respectivo Analyzer
- Electrum e o respectivo Analyzer
- Outras linguagens e ferramentas
- SMV e NuSMV
- TLA+ e a respectiva Toolbox
Docente / Horário
| Docente | Foto | Horário | Sala |
|---|---|---|---|
| Nuno Moreira Macedo |  | 5a-feira, 10h-12h (PL) | E7 1.10 |
| Manuel Alcino Cunha |  | 5a-feira, 9h-10h (T) | 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.
Método de avaliação
- 1 teste individual escrito (70%, ≥ 8)
- Data do teste: 9 de Janeiro de 2020
- Data do exame: 23 de Janeiro de 2020
- 2 trabalhos a realizar em grupos de 2 alunos (30%, ≥ 10)
Material pedagógico
Acetatos
- Apresentação da unidade curricular
- Electrum overview with the trash example
- First-Order Logic
- Relational Logic
- Alloy's type system
- Relational model finding
- First-order Linear Temporal Logic
- FO-LTL bounded model checking
- Safety, liveness, and fairness
- Methodology and tips for Alloy/Electrum
- Computation Tree Logic
- Introdução ao (Nu)SMV
- CTL model checking
- LTL model checking
Exercícios
- Electrum e Alloy
- Trash
- Trash FOL
- Classroom FOL
- Trash RL
- Classroom RL
- Graphs
- LTS
- CV Management
- Production Lines
- Modelar a estrutura do jogo Monopólio
- Trash LTL
- Leader election
- Modelar a estrutura e o comportamento de um circular buffer, e verificar que:
- Qualquer valor lido foi previamente escrito
- Se escrever é impossível, escritas apenas vão ocorrer após uma leitura
- Assumindo weak fairness para a leitura, todos os valores escritos serão lidos
- SMV / TLA+
- Ficha de exercícios SMV
- Numéricos
- Multiplicação por somas sucessivas
- Quadrados por soma de ímpares
- Máximo divisor comum com algoritmo de Euclides
- Algoritmos
- Modelar e verificar o algoritmo de exclusão mútua de Peterson
- Modelar e verificar o algoritmo de exclusão mútua de Dekker
- Modelar e verificar o algoritmo de exclusão mútua de Peterson generalizado para N processos (para SMV, N = 3 fixo)
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)
Enunciados dos trabalhos
Os carros modernos oferecem várias funcionalidades de segurança e conforto baseadas em componentes de software. Em particular, são já comuns atualmente sistemas de luzes exteriores adaptativos e de controlo de velocidade. Estes sistemas recolhem informação tanto de sensores (e.g., de luminosidade ou de velocidade) e da interface com o condutor (e.g., botões ou opções no computador de bordo), que é depois usada para controlar os atuadores (e.g., luzes externas ou os travões). É também comum que estes sistemas sejam adaptáveis para diferentes mercados (e.g., carros vendidos na UE ou nos EUA têm que seguir diferentes regras). O seguinte apontador descreve possíveis requisitos para sistemas deste tipo, e foi lançado como desafio numa conferência sobre métodos formais como os que estudamos nesta UC. Disponibiliza também um conjunto de sequências de validação que exemplificam possíveis execuções do sistema.
Os grupos de trabalho devem estudar o documento de referência referido acima com atenção, por forma a perceberem bem qual é o problema que é abordado. Naturalmente, devido à natureza das ferramentas, aspetos contínuos como o tempo real e a velocidade terão que ser abstraídos. Não é também expectável que cada grupo modele todas as componentes do sistema, ficando à consideração de cada um que aspetos focar. O modelo deve no entanto ser suficientemente rico em estrutura e comportamento, e permitir a verificação de alguns dos requisitos. Algumas sugestões são:
- Focar-se apenas num sistema (e.g., o de luzes exteriores)
- Focar-se apenas numa das funcionalidade do sistema (e.g., luzes de direção)
- Focar-se apenas numa configuração concreta (e.g., mercado EU)
Trabalho 1 sobre Alloy/Electrum
O objetivo deste trabalho é desenvolver um modelo Electrum de (uma parte) deste sistema, assim como um theme que facilite a compreensão das instâncias. Os grupos deverão entregar por email o trabalho até à data limite de 4-Dec-2019 (um modelo Electrum, devidamente comentado, e o respetivo theme).
Trabalho 2 sobre SMV/TLA+
O objetivo deste trabalho é desenvolver um modelo em SMV ou TLA+ de (uma parte) deste sistema. Os grupos deverão entregar por email o trabalho até à data limite de 15-Jan-2020 (um modelo SMV ou TLA+, devidamente comentado).
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.
Ferramentas