Í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