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, assim como lógicas apropriadas.
O curso aborda, essencialmente, sistemas reactivos clássicos; serão brevemente mencionados sistemas com requisitos de resposta em tempo real e de reacção probabilística.
Resultados de Aprendizagem
- Identificar as noções de interacção, sistema de transição e processo na modelação de sistemas computacionais complexos.
- Criar, analisar, comparar e transformar modelos de sistemas reactivos.
- Formular e analisar propriedades sobre esses modelos, captando num nível de abstração elevado, aspectos concretos da computação reactiva (por exemplo, situações de deadlock ou livelock, problemas de exclusão mútua e controlo de recursos, configurações de serviços móveis, etc.).
- Conhecer e utilizar ferramentas computacionais de suporte. Labelled transition system
Programa
- Introdução aos sistemas reactivos: estado, comportamento, interacção e concorrência
- Sistemas de transição etiquetados
- Definições básicas
- simulação e bissimulação; bissimilaridade.
- Variantes: sistemas de tempo real, probabilísticos e quânticos.
- Álgebras de processos
- Acção, processo e comportamento.
- Modelação e cálculo de sistemas reactivos em CCS.
- Modelação e cálculo de sistemas reactivos em mCRL2.
- Lógicas para sistemas reactivos:
- Modalidade e lógica modal.
- Lógica de Hennessy-Milner e suas variantes.
- Equivalência modal e bissimilaridade.
- Propriedades comportamentais e sua verificação em mCRL2
Apoio
Slides (2017-18)
- Labelled Transition Systems 1
- Labelled Transition Systems 2
- Process Algebra 1
- Process Algebra 2
- Process Modelling in mCRL2
- Modal Logic for Processes
- The modal Mu-calculus
Exercícios
Lições (versão 2014-15)
- Lição 1 - Sistemas de Transição e Comportamento
- iLição 2 - Modelação de Processos
- Lição 3 - Cálculo de Processos
- Lição 4 - Estudo de Casos
- Lição 5 - Cálculo Pi
- Lição 6 - Lógicas para Processos
- Lição 7 - Estudo de Caso: Um Protocolo de Autenticação
Bibliografia base
- Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen, Jiri Srba. Reactive Systems: Modelling, Specification and Verification. CUP, 2007. [livro]
- Jan Friso Groote, Mohammad Reza Mousavi. Modeling and Analysis of Communicating Systems. MIT Press, 2008. [livro]
Bibliografia complementar
- 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
Links
Funcionamento
Docente
Avaliação
- Trabalho prático de caracter laboratorial (2, 15% cada): a entregar em 13 de Abril e 25 Maio
- Prova individual escrita (70%): 25 Maio (data provisória)
- As notas finais superiores ou iguais a 19 valores terão que ser defendidas em prova oral.
- CLASSIFICAÇÕES FINAIS: 27.06.2018
- RECURSO: 27.07.2018
Provas
Contacto
- Atendimento: Quarta 10-12 (por marcação)
- Email: lsb arroba di ponto uminho ponto pt
- Última actualização: 2018.03.27