Languages and Formal Methods

<#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.