Processos e Concorrência - Edição 2007-08
Í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
Acetatos
Exercícios
Software
Exemplos
Álgebra de Processos
Lições
Laboratório
Formulário
Provas de Avaliação
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
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)
24 Julho As notas da época de recurso estão disponíveis
aqui.
30 Junho As notas finais estão disponíveis
aqui.
29 Junho As notas do teste do módulo II estão disponíveis
aqui.
19 Junho O teste marcado para amanhã, dia 20, decorrerá na sala 2111.
17 Junho Aula extra para dúvidas, Quinta-feira, 19 de Junho, 10h no DI-A1.
5 Maio As notas do primeiro teste estão disponíveis
aqui.
1 Maio Actualizados os sumários e disponibilizados os resumos das Lições e ficha de trabalho sobre o CWB-NC.
3 Abr Já está disponível na secção de projectos um programa para converter ficheiros do Pipe para o SMV.
19 Fev Os sumários podem ser encontrados no calendário.
19 Fev As aulas começam no dia 25 de Fevereiro.
Manuel Alcino Cunha
Luís Soares Barbosa