Especificação e Modelação (H507O2)
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 principais
- Alloy (Electrum) e o respectivo Analyzer
- Outras linguagens e ferramentas
- TLA+ e a respectiva Toolbox
- SMV e NuSMV
Docente / Horário
| Docente | Foto | Horário | Sala |
|---|---|---|---|
| Manuel Alcino Cunha |  | 5a-feira, 9h-11h | CP1 1.21 |
Alunos
| # | Nome | Curso |
|---|---|---|
| a83916 | Ana João Dias de Almeida | MiEI |
| a85516 | António Manuel Carvalho Gonçalves | MiEI |
| a80453 | Bárbara Andreia Cardoso Ferreira | MiEI |
| a82529 | Carlos Manuel Marques Afonso | MiEI |
| a34900 | Cecília da Conceição de Oliveira Soares | MiEI |
| a67683 | César Eduardo da Silva Magalhães | MiEI |
| pg41842 | César Hugo Moreira da Silva | MEI |
| a80970 | Davide da Silva Matos | MiEI |
| a76089 | Etienne da Silva Filipe Amado da Costa | MiEI |
| a85731 | Gonçalo José Azevedo Esteves | MiEI |
| a86617 | Gonçalo Pinto Nogueira | MiEI |
| a81283 | Hugo Filipe Oliveira de Sousa Faria | MiEI |
| a85573 | Jorge Gabriel Alves Cerqueira | MiEI |
| a84776 | José Emanuel Silva Rodrigues | MiEI |
| pg42839 | José Gonçalo Macedo Costa | MEI |
| a84577 | José Pedro Oliveira Silva | MiEI |
| pg42840 | Leandro Filipe Pereira Lima | MEI |
| pg42842 | Luís Marques | MEI |
| a78566 | Marcos Daniel Teixeira da Silva | MiEI |
| a71407 | Maurício Zulueta Lima Salgado | MiEI |
| a85700 | Pedro Miguel Araújo Costa | MiEI |
| a84783 | Pedro Miguel Borges Rodrigues | MiEI |
| a86266 | Rafael Inácio Lourenço | MiEI |
| a75411 | Ricardo Guerra Leal | MiEI |
| a81716 | Rodolfo António Vieira da Silva | MiEI |
| a80789 | Rui Filipe Brito Azevedo | MiEI |
| pg36086 | Vítor Hugo Gonçalves Silva | MMC |
Método de avaliação
- 1 teste individual escrito (60%, ≥ 8)
- 1 trabalhos a realizar em grupos de 2 alunos (20%)
- Avaliação contínua (20%)
Material pedagógico
Acetatos
- Course presentation
- Electrum overview with a distributed transaction protocol
- First-order logic
- Relational logic
Exercícios
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)
Ferramentas