University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Analysis of liveness through proof.

Wei, Kun. (2006) Analysis of liveness through proof. Doctoral thesis, University of Surrey (United Kingdom)..

Available under License Creative Commons Attribution Non-commercial Share Alike.

Download (5MB) | Preview


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.

Item Type: Thesis (Doctoral)
Divisions : Theses
Authors :
Wei, Kun.
Date : 2006
Contributors :
Depositing User : EPrints Services
Date Deposited : 09 Nov 2017 12:17
Last Modified : 20 Jun 2018 11:24

Actions (login required)

View Item View Item


Downloads per month over past year

Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800