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
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
Funcionamento
Docente
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