Í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

Programa Resumido

• Sistemas reactivos
  • Sistemas reactivos: interacção e concorrência.
  • Sistemas de transição de estados.
  • Introdução às álgebras de processos.
  • Modelação de sistemas reactivos em CCS.
  • Cálculo de sistemas reactivos em CCS.
  • Especificação de propriedades: lógica de Hennessy-Milner e 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 resposta em tempo-real
  • Especificação e verificação de propriedades: extensões à lógica de Hennessy-Milner
• Laboratório: modelação e análise de sistemas reactivos em UPPAAL

Bibliografia

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

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

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

Software

• UPPAAL

Material de Apoio

Acetatos

• Labelled transition systems (I)
• Labelled transition systems (II)
• Introduction to process algebra
• Logics for processes (I)
• Logics for processes (II)
• Time-critical reactive systems (I)
• Time-critical reactive systems (II)
• Application: the Orc coordination language

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
• Ficha de Exercícios 6 (mini-projectos em UPPAAL)
• Exercício em UPPAAL (Train Gate): versão da ficha e versão estendida
• UPPAAL case-study: the Lamport protocol
• Ficha de pré-avaliação

Outros Textos

• Process Algebra (notas)

Funcionamento

Docente

• Luís Soares Barbosa

Avaliação

Prova individual escrita única (a realizar no dia 19 de Junho 2010) sujeita às restrições seguintes:

• A admissibilidade à realização do teste é condicionada à resolução e entrega de pelo menos 8 dos exercícios seleccionados em cada aula teórico-prática.
• As notas finais superiores ou iguais a 19 valores terão que ser defendidas em prova oral.

Classificações finais (Teste + mini-projecto Uppaal)

Classificações finais (Exame)

Horário

Atendimento

Docente	Horário	Telefone
LSB	2ª 14h-16h (por marcação)	604463

-- Luís Soares Barbosa - 18 Julho 2010