Embedding the Stable Failures Model of CSP in PVS

9 years 9 months ago
Embedding the Stable Failures Model of CSP in PVS
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 di...
Kun Wei, James Heather
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Where IFM
Authors Kun Wei, James Heather
Comments (0)