| Data e Horário | Atividade | Local/Meio |
| 21/8, 10 às 12 hs | Sala de aula M3 | |
| 23/8, 10 às 12 hs | Discutir conceitos de evento, comunicação, alfabeto, processo, e operadores básicos para projeto de processos | Sala de aula M3 |
| 28/8, 10 às 12 hs | Discutir e comparar operadores de escolha, discutir eventos compostos, processos especiais, e leis algébricas de CSP | Sala de aula M3 |
| 30/8, 10 às 12 hs | Discutir modelos semânticos e noções de refinamento para CSP, modelo de traces, relacionar as leis algébricas com os modelos, especificação de processos | Sala de aula M3 |
| 4/9, 10 às 12 hs | Utilizar FDR para verificar propriedades de vários processos | Laboratório C6 |
| 6/9, 10 às 12 hs | Discutir e comparar operadores para composição paralela (composição síncrona e alfabetizada) | Sala de aula M3 |
| 11/9, 10 às 12 hs | Discutir e comparar operadores para composição paralela (composição generalizada e entrelaçamento), discutir utilização de composição paralela para restrição de processos | Sala de aula M3 |
| 13/9, 10 às 12 hs | Utilizar FDR para verificar propriedades de vários processos | Laboratório C6 |
| 18/9, 10 às 12 hs | Discutir operador para esconder eventos | Sala de aula M3 |
| 20/9, 10 às 12 hs | Discutir operador para renomear eventos, visão geral do modelo de failures e failures-divergences, definir escopo dos sistemas a serem especificados | Sala de aula M3 |
| 25/9, 10 às 12 hs | Utilizar FDR para verificar propriedades de vários processos | Laboratório C6 |
| 27/9, 10 às 12 hs | Fazer o projeto dos aspectos concorrentes e distribuídos do sistema | Laboratório C6 |
| 2/10, 10 às 12 hs | Fazer o projeto dos aspectos concorrentes e distribuídos do sistema | Laboratório C6 |
| 4/10, 10 às 12 hs | Verificar propriedades do sistema utilizando FDR | Laboratório C6 |
| 9/10, 14 às 16 hs | Entregar e apresentar o projeto do sistema em CSP | Laboratório C6 |
| 11/10, 10 às 12 hs | Motivação e objetivos, introdução à segunda parte do curso | Sala de aula M3 |
| 16/10, 10 às 12 hs | Especificando com conjuntos | Sala de aula M3 |
| 18/10, 10 às 12 hs | Especificando com relações | Sala de aula M3 |
| 23/10, 10 às 12 hs | Especificando com funções | Sala de aula M3 |
| 25/10, 10 às 12 hs | Especificando com sequências e bags | Sala de aula M3 |
| 30/10, 10 às 12 hs | Resumo das construções sintáticas de Z | Sala de aula M3 |
| 1/11, 10 às 12 hs | A ferramenta Z-Eves | Laboratório C5 |
| 6/11, 10 às 12 hs | Acompanhamento dos projetos | Laboratório C5 |
| 8/11, 10 às 12 hs | Validade do estado inicial e
cálculo de pré-condicao |
Sala de aula M3 |
| 13/11, 10 às 12 hs | Refinamento de especificações | Sala de aula M3 |
| 15/11 | Feriado | |
| 20/11, 10 às 12 hs | Exercícios de refinamento | Sala de aula M3 |
| 22/11, 10 às 12 hs | Usando Z-Eves para provar refinamento | Laboratório C5 |
| 27/11, 10 às 12 hs | Combinando CSP e Z: CSP-Z | Sala de aula M3 |
| 29/11, 10 às 12 hs | Model-checking especificações em CSP-Z | Laboratório C5 |
| 4/12, 10 às 12 hs | Acompanhamento dos projetos | Laboratório C5 |
| 6/12, 10 às 12 hs | Exame Escrito, Entregar o projeto do sistema em CSP-Z | Sala de aula M3 |
| 11/12, 10 às 12 hs | Apresentar o projeto do sistema em CSP-Z | Laboratório C5 |
|
Augusto Sampaio (acas@cin.ufpe.br)
e Paulo Borba (phmb@cin.ufpe.br) |