Notas de Aula

1. Objetivos e programa, especificação versus implementação, sistemas sequenciais versus sistemas concorrentes e distribuídos, conceitos básicos.

   Transparências. Prefácio e Capítulo 0 do livro texto de CSP.

2. Evento, comunicação, alfabeto, processo, e operadores básicos para projeto de processos.

   Transparências. Páginas 13 a 21 do livro texto de CSP.

3. Operadores de escolha, processos especiais, e leis algébricas de CSP.

   Transparências. Páginas 22 a 34 do livro texto de CSP.

4. Modelos semânticos e noções de refinamento para CSP, modelo de traces, relacionamento das leis algébricas com os modelos, especificação de processos. 

   Transparências. Páginas 35 a 50 do livro texto de CSP. Páginas 3 a 6, Seção 2, e Apêndice A do manual de FDR.

5. Operadores para composição paralela (composição síncrona e alfabetizada).

   Transparências. Páginas 51 a 64 do livro texto de CSP.

6. Operadores para composição paralela (composição generalizada e entrelaçamento), utilização de composição paralela para restrição de processos.

   Transparências. Páginas 65 a 76 do livro texto de CSP. Páginas 7 a 10, e Seções 3 e 4 do manual de FDR.

7. Operador para esconder eventos.

   Transparências. Páginas 77 a 85 do livro texto de CSP.

8. Operador para renomear eventos, visão geral dos modelos de failures e failures-divergences.

   Transparências sobre o operador de renomeação. Transparências sobre os modelos de failures e failures-divergences. Páginas 86 a 98 do livro texto de CSP.

9. Motivação e objetivos, introdução à segunda parte do curso.

   Transparências.

10. Especificando com conjuntos

    Transparências.

11. Especificando com relações

    Transparências em http://www.di.ufpe.br/~if116/aulas.htm (aula5 e aula6)

12. Especificando com funções

    Transparências em http://www.di.ufpe.br/~if116/aulas.htm (aula7)

13. Especificando com sequências e bags

    Transparências em http://www.di.ufpe.br/~if116/aulas.htm (aula10 e aula11)

14. Resumo das construções sintáticas de Z

    Transparências em http://www.di.ufpe.br/~if116/aulas.htm (aula12)

15. Cálculo estruturado de pré-condição e exercícios

    Transparências em http://www.di.ufpe.br/~if116/aulas.htm (aula19)

16. Formalizando o conceito de refinamento e exercicios

    Transparências em http://www.di.ufpe.br/~if116/aulas.htm (aula23)

17. Usando o Z-Eves para provar refinamento

    Transparências em http://www.di.ufpe.br/~if116/aulas.htm (aula25)

18. CSP-Z e sua Verificação

    Transparências.

Augusto Sampaio  (acas@cin.ufpe.br) e Paulo Borba (phmb@cin.ufpe.br)