Este curso visa motivar, apresentar e exercitar o uso de técnicas para especificação e projeto de sistemas distribuídos de alta confiabilidade e qualidade. Em particular, o uso destas técnicas ajuda a garantir que um sistema distribuído tem certas propriedades como ausência de impasse (deadlock) e compatibilidade entre a sua implementação final e a sua especificação inicial.
Primeiro vemos como os aspectos concorrentes dos sistemas distribuídos podem ser especificados e validados usando a linguagem CSP (Communicating Sequential Processes) e a ferramenta FDR. Em seguida mostramos como os aspectos sequenciais dos sistemas distribuídos podem ser especificados, validados e animados usando a linguagem Z e as ferramentas Z-EVES e ZANS. Por fim, apresentamos como estas duas linguagens podem ser integradas para especificar sistemas distribuídos. A ênfase não é em apresentar todos os detalhes de Z e CSP, mas apenas os detalhes básicos relevantes para a especificação e projeto de sistemas distribuídos.
Este curso é particularmente interessante para quem deseja desenvolver sistemas distribuídos complexos e confiáveis, mas também é importante para quem está interessado em aspectos de segurança, interoperabilidade, arquitetura e integração de sistemas, além de novas linguagens concorrentes e distribuídas para a Internet e WWW.