Especificação e Modelação
Docente e horário
| Docente | Foto | Horário | Sala |
|---|---|---|---|
| Manuel Alcino Cunha |  | 5a-feira, 9h-12h | Sala 1.16 (antiga 1.08) |
Método de avaliação
Notas
Enunciado do trabalho sobre NuSMV
O artigo Modelling an Aircraft Landing System in Event-B descreve a modelação formal de um sistema de controlo do trem de aterragem de um avião baseado nos requisitos impostos pela Federal Aviation Administration dos EUA. Neste artigo o trem de aterragem é modelado a níveis diferentes de abstracção, dando origem a vários modelos nomeados M1, M2, M3, etc, com cada vez mais detalhe.
Os grupos de trabalho devem estudar o artigo 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 Event-B, mas apenas na medida do que é necessário para perceberem o artigo. O que se pretende neste trabalho é exprimir os diferentes modelos M1, M2, M3, etc, usando o NuSMV em vez de Event-B. O nível de detalhe a atingir fica à consideração de cada grupo.
Os grupos deveram entregar por email o trabalho até à data limite de 15-Dez-2017 (um ficheiro zip com todos os modelos desenvolvidos, devidamente comentados).
Enunciado do trabalho sobre Alloy
O Monopólio é um dos jogos de tabuleiro mais populares em todo o mundo. O objectivo deste trabalho é fazerem um modelo Alloy deste jogo, cujas regras podem ser encontradas aqui. Naturalmente, por questões de eficiência na análise será necessário abstrair certos aspectos do jogo (por exemplo, a configuração exacta do tabuleiro ou os valores monetários envolvidos nas transacções), podendo cada grupo escolher diferentes aspectos a abstrair. Fica também à consideração de cada grupo a escolha do idioma de Alloy a usar na modelação da dinâmica do jogo, assim como a escolha das propriedades a verificar. 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 21-Jan-2018 (um modelo Alloy, devidamente comentado, e o respectivo theme).
Material pedagógico
- Modeling Specification (and Verification): slides introdutórios.
- Model Checking: slides de introdução ao model checking.
- NuSMV 2.6 User Manual.
- Exercícios sobre SMV.
- Exemplos SMV: cadeira.smv, farmer.smv, peterson_nomodules.smv, peterson_modules.smv.
- An Introduction to Alloy.
- Verifying Safety & Liveness in Alloy.
- Alloy: Under the Hood: breve apresentação da semântica, sistema de tipos, e arquitectura de verificação do Alloy.
- Exercícios sobre Alloy.
- Exemplos Alloy: avo.als, avo_event.als
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