Interacção e Concorrência - Edição 2014-15
Í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, 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.
Programa Resumido
- Introdução aos sistemas reactivos: estado, comportamento, interacção e concorrência.
- Sistemas de transição etiquetados: comportamento, processo, bissimulação, bissimilaridade.
- Cálculo de sistemas reactivos 1: Modelação e cálculo de sistemas reactivos em CCS.
- Cálculo de sistemas reactivos 2: 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; Mu-calculus modal; taxonomia de propriedades.
- Cálculo de sistemas reactivos 3: Mobilidade e o Pi-calculus.
- Laboratório: modelação e análise de sistemas reactivos em mCRL2
Bibliografia base
Bibliografia complementar
Software
Material de Apoio
Lições
Lição 1 - Sistemas de Transição e Comportamento
Liçã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
Acetatos
Sistemas de transição etiquetados
Bisimilaridade
Abstracção comportamental
Álgebra de processos (1)
Álgebra de processos (2)
Introdução à modelação em mCRL2
Lógicas para processos: Lógica de Hennessy-Milner
Lógicas para processos: Mu-calculus
Exercícios
Folha de Exercícios 1
Folha de Exercícios 2
Folha de Exercícios 3
Folha de Exercícios 4
Folha de Exercícios 5
Folha de Exercícios 6
Exemplos mCRL2
Funcionamento
Docente
Avaliação
- Prova individual escrita (70%)
- Teste prático de caracter laboratorial (30%)
- As notas finais superiores ou iguais a 19 valores terão que ser defendidas em prova oral.
Provas
Teste
Teste Prático
Exame Recurso
Horário
Atendimento
--
Luís Soares Barbosa - 11 Julho 2015, 1.27h
Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.