Redes de Petri + Lógica Temporal

Bibliografia

• Petri Nets for Systems Engineering: A Guide to Modeling, Verification, and Applications. Claude Girault and Rüdiger Valk (editors). Springer-Verlag, 2003.
• Elements of Distributed Algorithms: modeling and analysis with petri nets. Wolfgang Reisig. Springer-Verlag, 1998.
• Model Checking. Edmund M. Clarke Jr., Orna Grumberg, and Doron A. Peled. MIT Press, 2001.

Acetatos

• Redes de Petri
• Lógica Temporal
• Verificação por Modelos

Exercícios

• Ficha 1: Modelação com redes de Petri.
• Ficha 2: Exercícios sobre redes de Petri.
• Ficha 3: Verificação de propriedades sobre redes de Petri.
• Ficha 4: Especificação de propriedades usando lógica temporal.
• Ficha 5: Verificação directa de fórmulas CTL.
• Ficha 6: Verificação por modelos em SMV.

• Exercícios usados em exames anteriores.

Software

• PIPE2
• DaNAMiCS
• SMV (binário para Mac Os X)

Exemplos

• Leitores e Escritores (PIPE2)
• Princesa e Rãs (PIPE2)
• Call for Papers (PIPE2)
• Exclusão Mútua (SMV)
• Biblioteca (SMV)

Álgebra de Processos

Lições

• Lição 1: Contexto, Objectivos e Plano (inclui as referências bibliográficas para este módulo)
• Lição 2: Sistemas de Transição e Comportamento
• Lição 3: Modelação de Processos em CCS
• Lição 4: Cálculo de Processos
• Lição 5: Estudo de Casos
• [][Lição 6: Mobilidade e o Cálculo Pi]]

Laboratório

• Animação de Processos no CWB - NC

Formulário

• (para uso nas provas de avaliação)

Provas de Avaliação

• Correcção do Teste de 2008.06.12