University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Embedding the stable failures model of CSP in PVS

Wei, K and Heather, J (2005) Embedding the stable failures model of CSP in PVS Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3771 L. pp. 246-265.

[img]
Preview
PDF
csppvs.pdf
Available under License : See the attached licence file.

Download (212kB)
[img]
Preview
PDF (licence)
SRI_deposit_agreement.pdf

Download (33kB)

Abstract

We present an embedding of the stable failures model of CSP in the PVS theorem prover. Our work, extending a previous embedding of the traces model of CSP in [6], 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 analyzing infinite-state systems with an arbitrary number of components. We demonstrate the power of this 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' [21], with any number of dimensions, is deadlock-free. We have established some generic proof tactics for verification of properties of networks with many components. In addition, our technique of integrating FDR and PVS in our demonstration allows for handling of systems that would be difficult or impossible to analyze using either tool on its own. © Springer-Verlag Berlin Heidelberg 2005.

Item Type: Article
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
AuthorsEmailORCID
Wei, KUNSPECIFIEDUNSPECIFIED
Heather, JUNSPECIFIEDUNSPECIFIED
Date : 2005
Identification Number : 10.1007/11589976_15
Additional Information : The original publication is available at http://www.springerlink.com
Depositing User : Symplectic Elements
Date Deposited : 12 Feb 2013 11:50
Last Modified : 18 Sep 2014 01:48
URI: http://epubs.surrey.ac.uk/id/eprint/738615

Actions (login required)

View Item View Item

Downloads

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