20 Fev Os sumários podem ser encontrados no calendário.

22 Abr Ao contrário do que havia sido anunciado, haverá aula amanhã, dia 23, no horário habitual.

25 Abr Slides sobre Mu-calculus disponíveis na secção de Material

25 Abr Por razões imprevistas, não haverá aula prática amanhã, dia 26 de Abril.

5 Jun A ficha de pré-avaliação está on-line. Boa sorte!

18 Jun O teste será amanhã, dia 19 de Junho, 9.30 h, na sala 1220

24 Jun Classifcações finais do 1 semestre já estão on-line.

Interacção e Concorrência - Edição 2013-14

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

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.
• Álgebras de Processos
  • 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 e híbridas.
  • Lógicas temporais.
  • Especificação de propriedades e sua verificação.
  • Introdução às técnicas de model-checking.

• 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
• Tutorial sobre mCRL2 (Keiren, Ploeger, de Vink)

Material de Apoio

Acetatos

Sistemas de transição etiquetados

Simulação e bissimulação

Álgebra de processos

Introdução à modelação de processos em mCRL2

Lógica modal sobre processos

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

Projectos

Projectos em mCRL2 (Parte 1)

Docente

• Luís Soares Barbosa

Avaliação

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

Provas

Aviso (Provas orais)

As orais realizam-se no dia 18 de Julho, sexta-feira, entre as 10 e as 13h no gabinete do docente. A não comparência determina automaticamente a reprovação na UC

Horário

Atendimento

-- Luís Soares Barbosa - 18 Julho 2014, 21.45h

Í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

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

• Jan Friso Groote, Mohammad Reza Mousavi. Modeling and Analysis of Communicating Systems. MIT Press, 2008.

Bibliografia complementar

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

• 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

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

• Luís Soares Barbosa

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.

• Classificações
• Classificações após recurso

Provas

Teste

Teste Prático

Exame Recurso

Horário

Atendimento

-- Luís Soares Barbosa - 11 Julho 2015, 1.27h

Índice

Apresentação

Esta disciplina tem por objectivo introduzir técnicas de modelação e análise de sistemas concorrentes ou reactivos. Serão apresentadas duas abordagens distintas a este problema.

A primeira baseia-se na utilização de redes de Petri e lógica temporal. As redes de Petri são um modelo gráfico muito poderoso para representar sistemas concorrentes de média e alta complexidade. Algumas propriedades de sistemas concorrentes podem ser verificadas com técnicas de análise directa das redes, mas para especificar propriedades mais complexas será introduzida a lógica temporal. Esta lógica possui operadores modais específicos que nos permitem descrever a evolução do estado da computação ao longo do tempo. Em particular, será utilizada a lógica de tempo ramificado CTL, para a qual serão apresentadas diferentes técnicas de verificação de modelos. Esta abordagem será aplicada na modelação e análise de algoritmos clássicos da programação concorrente, protocolos de comunicação simples, e sistemas de controle de produção. Na componente prática laboratorial serão utilizadas ferramentas para edição gráfica de redes de Petri e para verificação simbólica de modelos.

Muitos modelos para a computação reactiva evoluiram a partir da noção de autómato, da qual retêm a estrutura de transições etiquetadas --- precisamente pelas interacções em que o sistema se envolve. Tais sistemas exibem comportamentos --- usualmente designados por processos --- que podem ser descritos por linguagens formais e que, mais importante ainda, formam domínios nos quais se podem definir (ou identificar) determinadas estruturas algébricas. I.e., operadores que os combinam e que exibem um conjunto suficientemente rico de propriedades que permitem combinar os padrões de interacção dos vários sistemas em presença. É esta a área de um conjunto de abordagems que exploram a estrutura algébrica dos comportamentos de sistemas reactivos e que se popularizou, a partir de finais dos anos '70 sob a designação de álgebras de processos.

A segunda parte desta disciplina recorre precisamente a duas álgebras de processos (o CCS e o cálculo Pi) para modelar as interacções e evolução dos sistemas reactivos, estudar a sua composicionalidade, definir equivalências entre eles, identificar propriedades e raciocinar equacionalmente sobre elas. O cálculo Pi, em particular, irá permitir-nos discutir formalmente acerca de sistemas reactivos cuja estrutura de interacções se altera dinamicamente ao longo da computação.

Programa Resumido

Redes de Petri

• Modelação de sistemas concorrentes com redes de Petri.
• Semântica operacional baseada em sistemas de transição de estados.
• Propriedades fundamentais de redes: finitude, animação e invertibilidade.
• Cálculo de invariantes de estado.
• Extensões às redes não coloridas: lugares com capacidade explicita e arcos inibidores.
• Ferramentas para especificação e animação de redes de Petri (DaNAMiCS, PEP).

Lógica Temporal

• Especificação de propriedades de segurança e animação usando lógica temporal CTL.
• Representação mínima de fórmulas CTL.
• Verificação directa de modelos para a lógica CTL.
• Representação da relação de acessibilidade usando lógica proposicional.
• Verificação simbólica de modelos para a lógica CTL baseada em OBDDs.
• Ferramentas para verificação simbólica de modelos (SMV).

Álgebra de Processos

• Autómatos e sistemas de transição. Interacção e comportamento.
• Modelação de sistemas reactivos em CCS. Semântica operacional. Análise e verificação de transições.
• Cálculo de sistemas reactivos. Equivalência estrita e observacional em CCS. Teorema da expansão. Resolução de equações.
• Cálculo de sistemas móveis. Motivação, sintaxe, semânticas e equivalências entre processos móveis.
• Animação e análise de processos no CWB e no MWB.

Material de Apoio

Redes de Petri + Lógica Temporal

Bibliografia

• Petri Nets for Systems Engineering: A Guide to Modeling, Verification, and Applications. Claude Girault and Rüdiger Valk (editors). Springer-Verlag, 2003.
• Elements of Distributed Algorithms: modeling and analysis with petri nets. Wolfgang Reisig. Springer-Verlag, 1998.
• Model Checking. Edmund M. Clarke Jr., Orna Grumberg, and Doron A. Peled. MIT Press, 2001.

Acetatos

• Redes de Petri
• Lógica Temporal
• Verificação por Modelos

Exercícios

• Ficha 1: Modelação com redes de Petri.
• Ficha 2: Exercícios sobre redes de Petri.
• Ficha 3: Verificação de propriedades sobre redes de Petri.
• Ficha 4: Especificação de propriedades usando lógica temporal.
• Ficha 5: Verificação directa de fórmulas CTL.
• Ficha 6: Verificação por modelos em SMV.

• Exercícios usados em exames anteriores.

Software

• PIPE2
• DaNAMiCS
• SMV (binário para Mac Os X)

Exemplos

• Leitores e Escritores (PIPE2)
• Princesa e Rãs (PIPE2)
• Call for Papers (PIPE2)
• Exclusão Mútua (SMV)
• Biblioteca (SMV)

Álgebra de Processos

Lições

• Lição 1: Contexto, Objectivos e Plano (inclui as referências bibliográficas para este módulo)
• Lição 2: Sistemas de Transição e Comportamento
• Lição 3: Modelação de Processos em CCS
• Lição 4: Cálculo de Processos
• Lição 5: Estudo de Casos

Laboratório

• Animação de Processos no CWB - NC

Formulário

• (para uso nas provas de avaliação)

Provas de Avaliação

• Correcção do Teste de 2008.06.12

Projectos

Pipe2smv

Conversor de ficheiros do Pipe para o formato do SMV. Todos os lugares devem ter capacidade limitada, ou então usar a opção -c para definir a capacidade máxima. A aplicação ainda está em fase de testes: não é garantido que todas as conversões estejam perfeitas, mas para a maior parte dos casos funciona bem.

Download (pipe2smv_bin.rar).

Trabalho realizado por Hugo Maia e Bruno Lopes.

Funcionamento

Equipa docente

• Manuel Alcino Cunha: Redes de Petri + Lógica Temporal.
• Luís Soares Barbosa: Álgebra de Processos.

Avaliação

Cada aluno deve escolher um dos seguintes métodos de avaliação:

• Realização de duas provas individuais escritas (50% + 50%).
• Realização de duas provas individuais escritas (35% + 35%) e de um pequeno projecto prático (30%).

As notas finais superiores ou iguais a 18 valores terão que ser defendidas numa prova extra.

A meio do semestre será realizado um teste sobre a primeira parte da matéria (redes de Petri + lógica temporal) e no final do semestre um segundo teste sobre a segunda parte da matéria (álgebra de processos). Os alunos com aprovação numa das partes ficam dispensados de responder às questões sobre essa matéria no exame de recurso. A nota mínima em cada uma das partes é de 8 valores.

Horário

Atendimento

Avisos (edição 2007-08)

Manuel Alcino Cunha
Luís Soares Barbosa

Í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
• sistemas reactivos móveis

Programa Resumido

• Sistemas reactivos
  • Sistemas reactivos: interacção e concorrência.
  • Sistemas de transição, comportamento e bisimilaridade.
  • Introdução às álgebras de processos.
  • Modelação e cálculo de sistemas reactivos em CCS.
  • Álgebras de processos com dados
  • Especificação de propriedades: 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 mobilidade
  • Especificação e verificação de propriedades: extensões à lógica de Hennessy-Milner
• Sistemas reactivos com requisitos de mobilidade
  • Mobilidade e interacção
  • Cálculo de sistemas reactivos com requisitos mobilidade: o Pi-calculus

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

Bibliografia

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

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

Software

• mCRL2
• UPPAAL

Material de Apoio

Acetatos

• Labelled transition systems (I)
• Labelled transition systems (II)
• Introduction to process algebra (I) - revised -
• Logics for processes (I)
• Logics for processes (II)
• Introduction to mCRL2 and mini project
• Introduction to ORC

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

Funcionamento

Docente

• Luís Soares Barbosa

Avaliação

• Prova individual escrita única (80%)
• Exercícios de realização individual e discussão nas aulas (20%)
• As notas finais superiores ou iguais a 19 valores terão que ser defendidas em prova oral.

• Classificações em Junho 2011 (teste + exercícios, ponderadas): disponíveis aqui
• Classificações finais (teste + exercícios, ponderadas + recurso): disponíveis aqui

Horário

Atendimento

-- Luís Soares Barbosa - 27 Julho 2011

Í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

Pipe2smv

Conversor de ficheiros do Pipe para o formato do SMV. Todos os lugares devem ter capacidade limitada, ou então usar a opção -c para definir a capacidade máxima. A aplicação ainda está em fase de testes: não é garantido que todas as conversões estejam perfeitas, mas para a maior parte dos casos funciona bem.

Download (pipe2smv_bin.rar).

Trabalho realizado por Hugo Maia e Bruno Lopes.

.natBreadCrumbs { width:0px; height:0px; overflow:hidden; }

.avisos { color: #444; font-size:12px; }

.natMainFooterContents, .natMainHeaderContents { padding:0px; margin:0px 0px; }

See also the faster WebTopicList

• TWikiGuest - example@your.company

Web Changes Notification Service

Each TWiki web has an automatic e-mail notification service that sends you an e-mail with links to all of the topics modified since the last alert.

Users subscribe to email notifications using their WikiName or an alternative email address, and can specify the webs/topics they wish to track using one of these bullet list formats:

three spaces * [ webname . ] wikiName - SMTP mail address
three spaces * [ webName . ] wikiName
three spaces * SMTP mail address
three spaces * SMTP mail address : topics
three spaces * [ webname . ] wikiName : topics

In the above examples, topics is a space-separated list of topic names. The user may further customize the specific content they will receive using the following formats:

• Specify topics without a Web. prefix
• Topics must exist in this web.
• Topics may be specified using * wildcards
• Each topic may optionally be preceded by a '+' or '-' sign. The '+' sign means "subscribe to this topic" (the same as not putting anything). The '-' sign means "unsubscribe" or "don't send notifications regarding this topic". This allows users to elect to filter out certain topics (and their children, to an arbitrary depth). Topic filters ('-') take precedence over topic includes ('+').
• Each topic may optionally be followed by an integer in parentheses, indicating the depth of the tree of children below that topic. Changes in all these children will be detected and reported along with changes to the topic itself. Note This uses the TWiki "Topic parent" feature.
• Each topic may optionally be immediately followed by an exclamation mark ! or a question mark ? with no intervening spaces, indicating that the topic (and children if there is a tree depth specifier as well) should be mailed out as complete topics instead of change summaries. ! causes the topic to be mailed every time even if there have been no changes, ? will mail the topic only if there have been changes to it. This only makes sense for subscriptions.

For example: Subscribe Daisy to all changes to topics in this web.

   * daisy.cutter@flowers.com

   * daisy.cutter@flowers.com: Web*

   * TWiki.DaisyCutter: Petal* (1) TWiki.WeedKillers (3) Pretty*Flowers

   * TWiki.StarTrekFan: Star* - *Wars - *sInTheirEyes - *shipTroopers

   * daisy@flowers.com: TWiki.NewsLetter?

   * buttercup@flowers.com: TWiki.NewsLetter! (1)

   * TWiki.GardenGroup: TWiki.AllNewsLetters? (3)
   * petunia@flowers.com: - TWiki.ManureNewsLetter

If a TWiki group is listed for notification, the group will be recursively expanded to the e-mail addresses of all members.

Tip: List names in alphabetical order to make it easier to find the names.

Note for System Administrators: Notification is supported by an add-on to the TWiki kernel called the MailerContrib. See the MailerContrib topic for details of how to set up this service.

Note: If you prefer a news feed, point your reader to WebRss (for RSS 1.0 feeds) or WebAtom (for ATOM 1.0 feeds). Learn more at WebRssBase and WebAtomBase, respectively.

Related topics: WebChangesAlert, TWikiUsers, TWikiRegistration

Advanced Search

Search: \.*