Elementos Lógicos da Programação 3

Licenciatura em Matemática e Ciências da Computação
3º Ano - 2º Semestre
Ano lectivo 2004-2005

Responsável

• JoseManuelValenca

Equipa Docente

Horário das Aulas

• Teórica: 3a das 11:00 às 13:00 (DI A1)
• Teórico-prática:
  • TP1 - 2a das 11:00 às 13:00 (DI 0.11)
  • TP2 - 5a das 11:00 às 13:00 (DI 0.11)

Programa Detalhado

• Redes de Petri
  • Modelação de sistemas concorrentes com redes de Petri.
  • Cálculo de matrizes de incidência.
  • Semântica operacional baseada em sistemas de transição de estados.
  • Propriedades fundamentais de redes: finitude, animação e invertibilidade.
  • Cálculo de invariantes de estado.
  • Extensões às redes não coloridas: lugares com capacidade explicita e arcos inibidores.
  • Redes coloridas.
  • Ferramentas para especificação e animação de redes de Petri (DaNAMiCS, PEP).
• Verificação de modelos
  • Especificação de propriedades de segurança e animação usando lógica temporal.
  • Lógicas CTL*, CTL e LTL.
  • Representação mínima de fórmulas CTL.
  • Verificação directa de modelos para a lógica CTL.
  • Representação da relação de acessibilidade usando lógica proposicional.
  • Verificação simbólica de modelos para a lógica CTL baseada em OBDDs.
  • Ferramentas para verificação simbólica de modelos (SMV).

Critério de Avaliação

• Hipótese 1
  • Exame Teórico (100%)
• Hipótese 2
  • Exame Teórico (60%, com nota mínima de 8 valores) + Projecto Prático (40%)

• Notas finais época recurso (notas)
• Notas finais época normal (notas)
• Notas finais época especial (notas)

Exames

• 1a Chamada (exame, notas)
• 2a Chamada (exame, notas)
• Recurso (exame)

Exemplos

• Aula 2
  • Partida (bim) e Corrida (bim)
  • Semáforo seguro (bim) e justo (bim)
• Aula 3
  • Produtor consumidor (bim)
• Aula 4
  • Produtor consumidor com 2 buffers sequenciais (bim) e paralelos (bim)
  • Bolas vermelhas e pretas (bim)
• Aula 5
  • 2 produtores com prioridade (bim) e depois do unfold (bim).
  • Biblioteca (bim, bim, bim) e depois do unfold (bim)
  • Conferência (bim)
• SMV
  • Exclusão mútua (smv), biblioteca (smv) e cache (smv)
• Exames
  • Rãs e Princesa normal (bim) e de 3 em 3 (bim).
  • Elevador (smv)
  • Slot machine (bim) sem moedeiro temporário (bim).
  • Braço mecânico (bim)
  • Exercício 3 da 2a chamada (smv).

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.

Apontadores WEB

• Petri Net World
• PIPE (zip)
• DaNAMiCS (tar.gz)
• PEP tool
• Integrated Network Analyser
• SMV Model Checker (binário)
• NuSmv Model Checker (uma variante Open Source do SMV)

Edições Anteriores

• 2003-2004