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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Brooke, P.: A Timed Semantics for a Hierarchical Design Notation. PhD thesis, University of York (1999)
Camilleri, A.J.: Higher order logic mechanization of the CSP failure-divergence semantics. Technical report, HP Lab Bristol (1990)
Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: A Refinement Strategy for Circus. Formal Aspects of Computing 15(2-3), 146–181 (2003)
Crow, J., Owre, S., Rushby, J., Shankar, N.: A tutorial introduction to PVS. In: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida (April 1995)
Crow, J., Owre, S., Rushby, J., Shankar, N.: PVS Prover Guide, PVS Language Reference, PVS System Guide. SRI International (2001)
Dutertre, B., Schneider, S.A.: Embedding CSP in PVS: an application to authentication protocols. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275. Springer, Heidelberg (1997)
Evans, N., Schneider, S.A.: Analysing Time Dependent Security Properties in CSP using PVS. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds.) ESORICS 2000. LNCS, vol. 1895. Springer, Heidelberg (2000)
Farmer, W.M., Guttman, J.D., Thayer, J.F.: IMPS: An Interactive Mathmetical Proof System. Journal of Automated Reasoning 11, 213–218 (1993)
Formal Systems (Europe) Ltd. Failures-Divergence Refinement—FDR 2 user manual (1997), Available from Formal Systems’ web site at, http://www.formal.demon.co.uk/FDR2.html
Isobe, Y., Roggenbach, M.: A generic theorem prover of CSP refinement. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 108–123. Springer, Heidelberg (2005)
Lazić, R.: A semantic study of data-independence with application to the mechanical verification of concurrent systems. PhD thesis, Oxford University (1999)
Meadows, C.A.: Open issues in formal methods for cryptographic protocol analysis. In: Gorodetski, V.I., Skormin, V.A., Popyack, L.J. (eds.) MMM-ACNS 2001. LNCS, vol. 2052, pp. 237–250. Springer, Heidelberg (2001)
Paulson, L.C.: A formulation of the simple theory of types (for isabelle). In: Martin-Löf, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 246–274. Springer, Heidelberg (1990)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall International, Englewood Cliffs (1998)
Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical compression for model-checking csp or how to check 1020 dining philosophers for deadlock. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 133–152. Springer, Heidelberg (1995)
Sampaio, A., Woodcock, J., Cavalcanti, A.: Refinement in Circus. In: Eriksson, L., Lindsay, P. (eds.) FME 2002. LNCS, vol. 2391, pp. 451–470. Springer, Heidelberg (2002)
Schneider, S.A.: Formal analysis of a non-repudiation protocol. In: Proceedings of the 11th IEEE Computer Security Foundations Workshop (1998)
Schneider, S.A.: Concurrent and real-time systems: the CSP approach. John Wiley & Sons, Chichester (1999)
Schneider, S.A., Bryans, J.: CSP, PVS and a Recursive Authentication Protocol. In: DIMACS Workshop on Formal Verification of Security Protocols (September 1997)
Tej, H., Wolff, B.: A corrected failure-divergence model for CSP in Isabelle/HOL. In: Fitzgerald, J.S., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313. Springer, Heidelberg (1997)
Yantchev, J., Jesshope, C.: Adaptive, low latency, deadlock-free packet routing for networks of processors. IEE Pro E (May 1989)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wei, K., Heather, J. (2005). Embedding the Stable Failures Model of CSP in PVS. In: Romijn, J., Smith, G., van de Pol, J. (eds) Integrated Formal Methods. IFM 2005. Lecture Notes in Computer Science, vol 3771. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11589976_15
Download citation
DOI: https://doi.org/10.1007/11589976_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30492-0
Online ISBN: 978-3-540-32240-5
eBook Packages: Computer ScienceComputer Science (R0)