Processos e Concorrência - Edição 2009-10

Í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)

André Silva	47408	16
Eduardo Fonseca	51176	11
João Rodrigues	50192	15
João Fonseca	47415	16
José Marques	50195	13
José Loureiro	50206	12
Manuel Sousa	50200	15
Marco Gomes	501971	10
Miguel Dias	51155	10
Nuno Marques	51164	10
Rui Peixoto	51166	11
Susana Vicente	30755	12
Tiago Côrte	46222	Exame

Classificações finais (Exame)

Ana Alexandra Costa	52856	17
Pedro Veloso	47422	10
Tiago Côrte	46222	12

Horário

Tipo	Horário	Sala
T	6ª 9h-11h	DI A2
TP	2ª 11h-13h	CP1 310

Atendimento

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

-- Luís Soares Barbosa - 18 Julho 2010