Elementos Lógicos da Programação III

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

Ùltima alteração: 12/07/2004

Avisos

• 29/07: Já disponíveis as notas da época de recurso (Notas).
• 12/07: Já disponíveis as notas da 1ª e 2ª chamadas (Notas).
• 07/05: Já disponível o enunciado dos projectos práticos.
• 22/03: Disponíveis duas novas secções nesta página: Elementos de Estudo e Apontadores WEB.
• 25/02: Nos dias 2 e 3 de Março (segunda e terça) não haverá aulas Teórico-Práticas de ElementosLogicosProgramacaoIII0304.
• 25/02: Este ano a página da disciplina é alojada no WIKI. Contacte um docente se pretender colaborar na manutenção da página.

Programa

Programa Resumido

• Redes de Petri
• Introdução aos modelos da concorrência
  • Sistemas de transição de estados: bissimulação.
  • Estruturas de eventos/redes de ocorrências.
• Redes de Petri coloridas
• Verificação de Modelos
  • Lógicas temporais: CTL e CTL+
  • Verificação simbólica

Programa Detalhado

Bibliografia

Bibliografia Recomendada:

• 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.

Elementos de Estudo

• 16/04 Uma nova versão do Animador que já suporta redes coloridas (Net2.tgz)
• 05/04 Nova verão dos módulos do Animador que fazem uso de multi-parameter type classes para permitir um maior nível de abstracção. (Net.tgz) --- Obs.: Para executar estes módulos devem-se passar as seguintes opções ao GHC: "-fglasgow-exts -fallow-undecidable-instances".
• 05/04 Versões simplificadas do animador de redes de Petri apresentado na teórica:
  • Versão I - Não define novas classes; utiliza o transformador de estados da biblioteca. (RPetri.hs)
  • Versão II - Evita a utilização do monad de estado. (RPetri2.hs)
• 05/04 Várias resoluções para os exercícios da aula sobre o Monad de Estado:
  • Versão I - Monad definido explicitamente (como foi apresentado na aula prática). (StateEx1.hs)
  • Versão II - Usando a biblioteca standard. (StateEx2.hs)
  • Versão III - Usando State threads. (StateEx3.hs)
• 22/03 Programa em Haskell para animação de Redes de Petri demonstrado nas aulas teóricas: (rp-jmv.tgz)

Apontadores WEB

• Petri Net World
• PEP tool
• Integrated Network Analyser
• SMV Model Checker
• NuSmv Model Checker (uma variante Open Source do SMV)

Projectos Práticos

• trabs.pdf

Horário e Equipa docente

• JoseManuelValenca (T)
• JoseBacelarAlmeida (TP)

Horário Lectivo:

Horário de Atendimento:

Critério de Avaliação

Nota final é calculada com base nas seguintes componentes:

Componente Teórica (Exame) - OBRIGATÓRIA - peso nunca inferior a 60% (nota mínima de 8 valores).
Componente Prática - FACULTATIVA - com peso máximo de 30%.

A componente prática consiste na realização de um projecto.

Notas

• Notas das épocas normais e de recurso (PDF)