Skip to main content
SpringerLink
Log in

Formalising an Integrated Language in PVS

  • Conference paper
Book cover Formal Methods and Software Engineering (ICFEM 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2885))

Included in the following conference series:

  • 411 Accesses

Abstract

System verification is one of the main topics of interest in formal methods. In this paper, we especially focus on equivalence proofs between abstract specification and more concrete ones. We propose an encoding into PVS of an integrated specification language. This language integrates the CCS process algebra extended to manage algebraic terms written from datatype definitions. Such an integrated language is useful to specify large size systems and to cover the different involved aspects. This encoding makes it possible the use of PVS for verification of nontrivial systems.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Brückner, B., Mosses, P.D., Sannella, D., Tarlecki, A.: CASL: The Common Algebraic Specification Language. Theoretical Computer Science 286(2), 153–196 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  2. Attiogbé, C., Francheteau, A., Limousin, J., Salaün, G.: ISA, a Tool for Integrated Specifications Animation, Available at http://www.sciences.univ-nantes.fr/info/perso/permanents/salaun/ISA/isa.html

  3. Basten, T., Hooman, J.: Process Algebra in PVS. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 270–284. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  4. Bodeveix, J.-P., Filali, M.: Type Synthesis in B and the Translation of B to PVS. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 350–369. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  5. Bodeveix, J.-P., Filali, M., Muñoz, C.: A Formalization of the B Method in Coq and PVS. In: Proc. of the B Users Group Meeting – Applying B in an industrial context: Tools, Lessons nd Techniques (FM 1999), pp. 32–48. Springer, Heidelberg (1999)

    Google Scholar 

  6. Bolognesi, T., Brinksma, E.: Introduction to the ISO Specification Language LOTOS. In: van Eijk, P.H.J., Vissers, C.A., Diaz, M. (eds.) The Formal Description Technique LOTOS, pp. 23–73. Elsevier Science Publishers North-Holland (1989)

    Google Scholar 

  7. Boulton, R., Gordon, A., Gordon, M.J.C., Herbert, J., van Tassel, J.: Experience with Embedding Hardware Description Languages in HOL. In: Proc. of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, The Netherlands. IFIP TC10/WG 10.2, pp. 129–156. North-Holland, Amsterdam (1992)

    Google Scholar 

  8. Brooke, P.: A Timed Semantics for a Hierarchical Design Notation. PhD Thesis, University of York (1999)

    Google Scholar 

  9. Calder, M., Maharaj, S., Shankland, C.: A Modal Logic for Full LOTOS Based on Symbolic Transition Systems. The Computer Journal 45(1), 55–61 (2002)

    Article  MATH  Google Scholar 

  10. Calder, M., Shankland, C.: A Symbolic Semantics and Bisimulation for Full LOTOS. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds.) Proc. of the International Conference on Formal Description Techniques for Networked and Distributed Systems (FORTE 2001), Korea. IFIP Conference Proceedings, vol. 197, pp. 184–200. Kluwer Academic Publishers, Dordrecht (2001)

    Google Scholar 

  11. Cleaveland, R., Li, T., Sims, S.: The Concurrency Workbench of the New Century (Version 1.2). Department of Computer Science, North Carolina State University (2000)

    Google Scholar 

  12. Crow, J., Owre, S., Rushby, J., Shankar, N., Srivas, M.: A Tutorial Introduction to PVS. In: Proc. of the Workshop on Industrial-Strength Formal Specification Techniques (WIFT 1995), USA. Computer Science Laboratory, SRI International (1995)

    Google Scholar 

  13. Dutertre, B., Schneider, S.: Using a PVS Embedding of CSP to Verify Authentication Protocols. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 121–136. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  14. Fernandez, J.-C., Garavel, H., Kerbrat, A., Mounier, L., Mateescu, R., Sighireanu, M.: CADP: A Protocol Validation and Verification Toolbox. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 437–440. Springer, Heidelberg (1996)

    Google Scholar 

  15. Fischer, C.: CSP-OZ: a Combination of Object-Z and CSP. In: Bowman, H., Derrick, J. (eds.) Proc. of the 2nd IFIP Workshop on Formal Methods for Open Object-Based Distributed Systems (FMOODS 1997), UK, pp. 423–438. Chapman and Hall, Boca Raton (1997)

    Google Scholar 

  16. Galloway, J., Stoddart, W.: An Operational Semantics for ZCCS. In: Hinchey, M.G., Liu, S. (eds.) Proc. of the 1st International Conference onf Formal Engineering Methods (ICFEM 1997), Japan, pp. 272–282. IEEE Computer Society Press, Los Alamitos (1997)

    Chapter  Google Scholar 

  17. Garland, S.J., Guttag, J.V.: A Guide to LP, the Larch Prover. Technical Report, Palo Alto, California (1991)

    Google Scholar 

  18. Garland, S.J., Guttag, J.V., Horning, J.J.: An Overview of Larch. In: Lauer, P.E. (ed.) Functional Programming, Concurrency, Simulation and Automated Reasoning. LNCS, vol. 693, pp. 329–348. Springer, Heidelberg (1993)

    Google Scholar 

  19. Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

  20. Gravell, A.M., Pratten, C.H.: Embedding a Formal Notation: Experiences of Automating the Embedding of Z in the Higher Order Logics of PVS and HOL. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 73–84. Springer, Heidelberg (1998)

    Google Scholar 

  21. Ingólfsdóttir, A., Lin, H.: A Symbolic Approach to Value-Passing Processes. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 427–478. Elsevier, Amsterdam (2001)

    Chapter  Google Scholar 

  22. ISO. LOTOS: a Formal Description Technique based on the Temporal Ordering of Observational Behaviour. Technical Report 8807, International Standards Organisation (1989)

    Google Scholar 

  23. Hennessy, M., Milner, R.: Algebraic Laws for Non-Determinism and Concurrency. Journal of the ACM 32, 137–161 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  24. Maharaj, S.: A PVS Theory of Symbolic Transition Systems. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 255–266. Springer, Heidelberg (2001)

    Google Scholar 

  25. Mahony, B., Dong, J.S.: Blending Object-Z and Timed CSP: An Introduction to TCOZ. In: Proc. of the International Conference on Software Engineering (ICSE 1998), Japan, pp. 95–104. IEEE Computer Society Press / ACM Press (1998)

    Google Scholar 

  26. Melham, T.F.: A Mechanized Theory of the π-calculus in HOL. Nordic Journal of Computing 1(1), 50–76 (1995)

    MathSciNet  Google Scholar 

  27. Milner, R.: Communication and Concurrency. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  28. Muñoz, C., Rushby, J.: Structural Embeddings: Mechanization with Method. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 452–471. Springer, Heidelberg (1999)

    Google Scholar 

  29. Nesi, M.: Formalising a Value-Passing Calculus in HOL. Formal Aspects of Computing 11(2), 160–199 (1999)

    Article  MATH  Google Scholar 

  30. Nipkow, T., Paulson, L.C.: Isabelle-91. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 673–676. Springer, Heidelberg (1992)

    Google Scholar 

  31. Pratten, C.H.: An Introduction to Proving AMN Specifications with PVS and the AMNPROOF Tool. In: Habrias, H. (ed.) Proc. of Z Twenty Years on - What is its Future, France, pp. 149–165 (1995)

    Google Scholar 

  32. Salaün, G., Allemand, M., Attiogbé, C.: Formal Framework for a Generic Combination of a Process Algebra with an Algebraic Specification Language: an Overview. In: Proc. of the 8th Asia-Pacific Software Engineering Conference (APSEC 2001), Macau, pp. 299–302. IEEE Computer Society Press, Los Alamitos (2001)

    Chapter  Google Scholar 

  33. Salaün, G., Allemand, M., Attiogbé, C.: A Method to Combine any Process Algebra with an Algebraic Specification Language: the π-Calculus Example. In: Proc. of the 26th Annual International Computer Software and Applications Conference (COMPSAC 2002), England, pp. 385–390. IEEE Computer Society Press, Los Alamitos (2002)

    Google Scholar 

  34. Salaün, G., Allemand, M., Attiogbé, C.: Specification of an Access Control System with a Formalism Combining CCS and CASL. In: Proc. of the 7th International Workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA 2002). IEEE Computer Society Press, USA (2002)

    Google Scholar 

  35. Salaün, G., Attiogbé, C., Allemand, M.: Verification of Integrated Specifications using PVS. Technical Report 03.02, University of Nantes (February 2003), Available at http://www.sciences.univ-nantes.fr/info/perso/permanents/salaun/papers/verif_ifm_with_pvs.ps

  36. Treharne, H., Schneider, S.: Using a Process Algebra to Control B OPERATIONS. In: Araki, K., Galloway, A., Taguchi, K. (eds.) Proc. of the 1st International Conference on Integrated Formal Methods (IFM 1999), UK, pp. 437–457. Springer, Heidelberg (1999)

    Google Scholar 

  37. van de Pol, J., Hooman, J., de Jong, E.: Modular Formal Specification of Data and Behaviour. In: Araki, K., Galloway, A., Taguchi, K. (eds.) Proc. of the 1st Conference on Integrated Formal Methods (IFM 1999), UK, pp. 109–128. Springer, Heidelberg (1999)

    Google Scholar 

  38. Woodcock, J., Cavalcanti, A.: The Semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IRIN, Université de Nantes, 2 rue de la Houssinière, B.P. 92208, 44322, Nantes Cedex 3, France

    Gwen Salaün & Christian Attiogbé

Authors
  1. Gwen Salaün
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christian Attiogbé
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing, National University of Singapore, Singapore

    Jin Song Dong

  2. University of York,  

    Jim Woodcock

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Salaün, G., Attiogbé, C. (2003). Formalising an Integrated Language in PVS. In: Dong, J.S., Woodcock, J. (eds) Formal Methods and Software Engineering. ICFEM 2003. Lecture Notes in Computer Science, vol 2885. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39893-6_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-39893-6_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-20461-9

  • Online ISBN: 978-3-540-39893-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation