Processos e Concorrência

Licenciatura em Ciências da Computação
Interacção e Concorrência - Edição 2013-14

Í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
    • Automatos e sistemas de transição.
    • 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

Bibliografia complementar

Software

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

tinynew.gif Aviso

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

Docente

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)

tinynew.gifClassificações Finais (épocas normal + recurso) --- CORRIGIDAS

tinynew.gifClassificações Época de Recurso

Provas

Entrega TP 30 Maio 2013
Teste 20 Junho 2013
Exame Recurso 12 Julho 2013

Horário

Tipo Horário Sala
TP 2ª 11h-13h CPII 307
T 4ª 09h-11h CPII 302

Atendimento

Docente Horário Telefone
LSB 4ª 11h-13h (por marcação) 604463

-- Luís Soares Barbosa - 23 Julho 2013, 18.00h

-- LuisSoaresBarbosa - 20 Feb 2014

r2 - 18 Feb 2015 - 01:22:52 - LuisSoaresBarbosa
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM