Abstract
Over the past decade, formal methods have been remarkably successful in their application to the analysis of concurrent systems. The vast bulk of work to date has been concerned only with safety properties and liveness properties however have not yet been mastered to the same degree. Broadly speaking, approaches to analysis of concurrent systems have fallen into two camps: model checking and theorem proving. Although both of them are rather successful, they suffer from their own deficiencies-that is, model checking is superior in checking a finite system automatically; theorem proving however can reason about systems with massive or infinite state spaces. In the thesis we present an embedding of the stable failures model of CSP in the theorem prover PVS. Our work, extending Dutertre and Schneider's traces embedding in PVS, provides a platform for the formal verification not only of safety specifications, but also of liveness specifications of concurrent systems in theorem provers. Such a platform is particularly good at analysing infinite-state systems with an arbitrary number of components. We have demonstrated the power of the CSP embedding by using it to construct formal proofs that the asymmetric dining philosophers problem with an arbitrary number of philosophers is deterministic and deadlock-free, and that an industrial-scale example, a 'virtual network', with any number of nodes, is deadlock-free. Also we use such an embedding to prove the correctness of the fairness property of the Zhou-Gollmann protocol. We discuss a potential way to widen the applicability of formal methods, along with developing a tool to automatically transform PVS scripts into FDR scripts, in order to unite the automatic nature of model checking and the generality of theorem proving.