intro.pdf
Acetatos: Apresentação da disciplina.
strans.pdf
Acetatos: Sistemas de transição.
petri.pdf
Acetatos: Redes de Petri.
temporal.pdf
Acetatos: Lógica temporal.
verification.pdf
Acetatos: Verificação por modelos.
ficha1.pdf
Ficha Prática 1: Sistemas de transição.
ficha2.pdf
Ficha Prática 2: Modelação com redes elementares.
ficha3.pdf
Ficha Prática 3: Exercícios sobre redes elementares.
ficha4.pdf
Ficha Prática 4: Modelação com redes P/T.
ficha5.pdf
Ficha Prática 5: Exercícios sobre redes P/T.
ficha6.pdf
Ficha Prática 6: Exercícios sobre redes P/T.
ficha7.pdf
Ficha Prática 7: Exercícios sobre redes coloridas.
ficha8.pdf
Ficha Prática 8: Especificação e verificação de fórmulas LTL.
ficha9.pdf
Ficha Prática 9: Verificação directa de fórmulas CTL usando pontos fixos.
ficha10.pdf
Ficha Prática 10: Verificação por modelos em SMV.
ficha11.pdf
Ficha Prática 11: Ordered Binary-Decision Diagrams.
perguntas.pdf
Exercícios de exames.
danamics-1.1.tar.gz
Ferramenta: editor de redes de Petri em Java. Versão sem restrições.
peterson.bim
Exemplo: algoritmo de Peterson para exclusão mútua.
crosstalk.bim
Exemplo: protocolo para detecção de conversas cruzadas.
maria.zip
Ferramenta: verificador de fórmulas LTL.
semaforo.pn
Exemplo: exclusão mútua com semáforo.
redblack.pn
Exemplo: bolas vermelhas e bolas pretas.
smv
Ferramenta: verificador simbólico de fórmula CTL.
mutual.smv
Exemplo: exclusão mútua com semáforo.
biblio.smv
Exemplo: utente de uma biblioteca.
notas.pdf
Notas finais.