Índice

Objectivos

Este curso tem por objectivo o estudo de sistemas reactivos, com ênfase na sua composição concorrente e no controlo da interacção continuada com o ambiente.

Serão introduzidas técnicas de especificação de propriedades, modelação, análise e verificação deste tipo de sistemas.

O curso aborda:

• sistemas reactivos clássicos (i.e., sem requisitos de resposta em tempo real)
• sistemas reactivos de tempo real
• sistemas reactivos móveis

Programa Resumido

• Sistemas reactivos
  • Sistemas reactivos: interacção e concorrência.
  • Sistemas de transição, comportamento e bisimilaridade.
  • Introdução às álgebras de processos.
  • Modelação e cálculo de sistemas reactivos em CCS.
  • Álgebras de processos com dados
  • Especificação de propriedades: Mu-calculus.
• Sistemas reactivos com requisitos de resposta em tempo-real
  • Autómatos com anotações temporais
  • Cálculo de sistemas reactivos com requisitos de mobilidade
  • Especificação e verificação de propriedades: extensões à lógica de Hennessy-Milner
• Sistemas reactivos com requisitos de mobilidade
  • Mobilidade e interacção
  • Cálculo de sistemas reactivos com requisitos mobilidade: o Pi-calculus

• Laboratório: modelação e análise de sistemas reactivos em mCRL2

Bibliografia

• J. C. M. Baeten, T. Basten, M. A. Reniers. Process Algebra: Equational Theories of Communicating Processes. CUP, 2010.

• Robin Milner. Communicating and Mobile Systems: The Pi Calculus. CUP, 1999.

• Christel Baier, Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008.

• Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen, Jiri Srba. Reactive Systems: Modelling, Specification and Verification. CUP, 2007.

Software

• mCRL2
• UPPAAL

Material de Apoio

Acetatos

• Labelled transition systems (I)
• Labelled transition systems (II)
• Introduction to process algebra (I) - revised -
• Logics for processes (I)
• Logics for processes (II)
• Introduction to mCRL2 and mini project
• Introduction to ORC

Exercícios

• Ficha de Exercícios 1
• Ficha de Exercícios 2
• Ficha de Exercícios 3
• Ficha de Exercícios 4
• Ficha de Exercícios 5

Funcionamento

Docente

• Luís Soares Barbosa

Avaliação

• Prova individual escrita única (80%)
• Exercícios de realização individual e discussão nas aulas (20%)
• As notas finais superiores ou iguais a 19 valores terão que ser defendidas em prova oral.

• Classificações em Junho 2011 (teste + exercícios, ponderadas): disponíveis aqui
• Classificações finais (teste + exercícios, ponderadas + recurso): disponíveis aqui

Horário

Atendimento

-- Luís Soares Barbosa - 27 Julho 2011