<#915#>#tex2html_wrap3868#<#915#>
This section of the book presents and outlines some of the
techniques used and being developed for distributed system
description or specification. We look in particular
at process algebras such as LOTOS and CSP,
and predicate calculus based languages such as Z.
Process algebras are good at analysing protocols to study liveness
properties e.g. the absence of deadlock. They are less good at
analysing and modelling internal state.
In contrast Z an similar formalisms are excellent at modelling state
and state changes which will be important in a system. There are less
good at for studying liveness properties.
There have been attempts to combine the strengths of both, but this is still the
subject of active research.