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
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
Exercícios
- Electrum e Alloy
- SMV / TLA+
- Ficha de exercícios SMV
- Numéricos
- Algoritmos
Leituras recomendadas
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
Ferramentas
