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

Programa Resumido

• Introdução aos sistemas reactivos: estado, comportamento, interacção e concorrência.
• Sistemas reactivos
  • Sistemas de transição etiquetados.
  • Processo e comportamento.
  • Similaridade e bisimilaridade.
  • Introdução às álgebras de processos.
  • Modelação e cálculo de sistemas reactivos em CCS e mCRL2.
  • Mobilidade e o Pi-calculus.
• Lógicas para sistemas reactivos
  • Lógica de Hennessy-Milner e suas extensões.
  • Lógicas modais, híbridas e temporais.
  • Especificação de propriedades e sua verificação.
  • Introdução às técnicas de model-checking.
• Sistemas reactivos com requisitos adicionais
  • Sistemas reactivos com requisitos de resposta em tempo-real
  • Sistemas reactivos com evolução probabilística

• Laboratório: modelação e análise de sistemas reactivos em mCRL2

Bibliografia base

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

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

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.

Software

• mCRL2

Material de Apoio

Acetatos

Sistemas de transição etiquetados

Simulação, bissimulação e bisimilaridade

Cálculo de processos

Introdução a mCRL2 (modelação)

Lógica de Hennessy-Milner

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

Folha de Exercícios 7

teste 11-12 exame 11-12

Funcionamento

Aviso

• em resposta a questão colocada pela Delegada de Curso, esclarece-se que as provas de avaliação serão sem consulta

Docente

• Luís Soares Barbosa

Avaliação

• Prova individual escrita única (80%)
• Trabalho prático de síntese de conhecimentos para realização em grupos de 2 elementos e discussão nas aulas (20%)
• As notas finais superiores ou iguais a 19 valores terão que ser defendidas em prova oral.

Teste com correcção

Classificações (época normal)

Classificações Finais (épocas normal + recurso) --- CORRIGIDAS

Classificações Época de Recurso

Provas

Horário

Atendimento

-- Luís Soares Barbosa