Document Open Access Logo

An Operational Semantics in Isabelle/HOL-CSP

Authors Benoît Ballenghien , Burkhart Wolff

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.7.pdf
  • Filesize: 0.86 MB
  • 18 pages

Document Identifiers

Author Details

Benoît Ballenghien
  • Laboratoire Méthodes Formelles, University Paris-Saclay, France
Burkhart Wolff
  • Laboratoire Méthodes Formelles, University Paris-Saclay, France

Funding

  • Ballenghien, Benoît: Labex DigiCosme.

Acknowledgements

We would like to thank Catherine Dubois for her remarks on earliest versions of this paper. The present version has been generated and deeply checked with Isabelle/DOF [Brucker and Wolff, 2022; Achim D. Brucker et al., 2023].

Cite AsGet BibTex

Benoît Ballenghien and Burkhart Wolff. An Operational Semantics in Isabelle/HOL-CSP. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.7

Abstract

The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today a reference model for concurrency. In the fairly rich literature, several versions of operational semantics have been discussed, which should be consistent with the denotational one. This work is based on Isabelle/HOL-CSP 2.0, a shallow embedding of the failure-divergence model of denotational semantics proposed by Hoare, Roscoe and Brookes in the eighties. In several ways, HOL-CSP is actually an extension of the original setting in the sense that it admits higher-order processes and infinite alphabets. In this paper, we present a construction and formal equivalence proofs between operational CSP semantics and the underlying denotational failure-divergence semantics. The construction is based on a definition of the operational transition operator P ⇝e P’ basically via the After operator and the classical failure-divergence refinement. Several choices are discussed to formally derive the operational semantics leading to subtle differences. The derived operational semantics for symbolic Labelled Transition Systems (LTSs) can be potentially used for certifications of model-checker logs as well as combined proof techniques.

Subject Classification

ACM Subject Classification
  • Theory of computation → Higher order logic
  • Theory of computation → Semantics and reasoning
  • General and reference → Verification
Keywords
  • Process-Algebra
  • Semantics
  • Concurrency
  • Computational Models
  • Theorem Proving
  • Isabelle/HOL

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. FDR4 - The CSP Refinement Checker. https://www.cs.ox.ac.uk/projects/fdr/, 2019.
  2. Jing An, Lei Zhang, and Chun You. The design and implementation of data independence in the csp model of security protocol. Advanced Materials Research, 915-916:1386-1392, April 2014. URL: https://doi.org/10.4028/www.scientific.net/AMR.915-916.1386.
  3. Benoît Ballenghien, Safouan Taha, and Burkhart Wolff. HOL-CSPM - Architectural operators for HOL-CSP. Archive of Formal Proofs, 2023, 2023. URL: https://www.isa-afp.org/entries/HOL-CSPM.html.
  4. Benoît Ballenghien and Burkhart Wolff. Operational Semantics formally proven in HOL-CSP. Archive of Formal Proofs, December 2023. URL: https://isa-afp.org/entries/HOL-CSP_OpSem.html.
  5. G. Barrett. Model checking in practice: the t9000 virtual channel processor. IEEE Transactions on Software Engineering, 21(2):69-78, February 1995. URL: https://doi.org/10.1109/32.345823.
  6. S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential processes. J. ACM, 31(3):560-599, 1984. Google Scholar
  7. S. D. Brookes and A. W. Roscoe. An improved failures model for communicating sequential processes. In Stephen D. Brookes, Andrew William Roscoe, and Glynn Winskel, editors, Seminar on Concurrency, pages 281-305, Berlin, Heidelberg, 1985. Springer. Google Scholar
  8. Achim D. Brucker, Idir Aït-Sadoune, Nicolas Méric, and Burkhart Wolff. Using deep ontologies in formal software engineering. In Uwe Glässer, José Creissac Campos, Dominique Méry, and Philippe A. Palanque, editors, Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Nancy, France, May 30 - June 2, 2023, Proceedings, volume 14010 of Lecture Notes in Computer Science, pages 15-32. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-33163-3_2.
  9. Achim D. Brucker and Burkhart Wolff. Isabelle/dof, July 2022. URL: https://doi.org/10.5281/zenodo.6810799.
  10. Albert J. Camilleri. A higher order logic mechanization of the csp failure-divergence semantics. In Graham Birtwistle, editor, IV Higher Order Workshop, Banff 1990, pages 123-150, London, 1991. Springer. Google Scholar
  11. Albert John Camilleri. Mechanizing CSP trace theory in higher order logic. IEEE Trans. Software Eng., 16(9):993-1004, 1990. Google Scholar
  12. Paolo Crisafulli, Safouan Taha, and Burkhart Wolff. Modeling and analysing cyber-physical systems in HOL-CSP. Robotics Auton. Syst., 170:104549, 2023. URL: https://doi.org/10.1016/J.ROBOT.2023.104549.
  13. Carlos Alberto da Silva Carvalho de Freitas. A theory for communicating, sequential processes in coq, 2020. URL: https://api.semanticscholar.org/CorpusID:259373665.
  14. A.A.A. Donovan and B.W. Kernighan. The Go Programming Language. Addison-Wesley Professional Computing Series. Pearson Education, 2015. Google Scholar
  15. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1985. Google Scholar
  16. Bashar Igried and Anton Setzer. Programming with monadic csp-style processes in dependent type theory. In Proceedings of the 1st International Workshop on Type-Driven Development, TyDe 2016, pages 28-38, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2976022.2976032.
  17. Bashar Igried and Anton Setzer. Trace and stable failures semantics for csp-agda. arXiv preprint arXiv:1709.04714, 2017. Google Scholar
  18. Yoshinao Isobe and Markus Roggenbach. A complete axiomatic semantics for the CSP stable-failures model. In CONCUR 2006 - Concurrency Theory, 17th International Conference, Bonn, Germany, August 27-30, 2006, pages 158-172, 2006. Google Scholar
  19. Yoshinao Isobe and Markus Roggenbach. Csp-prover: a proof tool for the verification of scalable concurrent systems. Information and Media Technologies, 5(1):32-39, 2010. URL: https://doi.org/10.11185/imt.5.32.
  20. He Jifeng and CAR Hoare. From algebra to operational semantics. Information Processing Letters, 45(2):75-80, 1993. Google Scholar
  21. Ranko S. Lazic. A semantic study of data-independence with applications to the mechanical verification of concurren. PhD thesis, University of Oxford, 1999. Google Scholar
  22. Olaf Müller, Tobias Nipkow, David von Oheimb, and Oskar Slotosch. HOLCF = HOL + LCF. j-fp, 9(2):191-223, 1999. URL: https://doi.org/10.1017/S095679689900341X.
  23. Pasquale Noce. Conservation of CSP noninterference security under sequential composition. Archive of Formal Proofs, 2016. URL: https://www.isa-afp.org/entries/Noninterference_Sequential_Composition.shtml.
  24. A. W. Roscoe. An alternative order for the failures model. J. Log. Comput., 2:557-577, 1992. Google Scholar
  25. A. W. Roscoe and Philippa J. Broadfoot. Proving security protocols with model checkers by data independence techniques. Journal of Computer Security, 7(1):147-190, 1999. Google Scholar
  26. A. W. Roscoe, P. H. B. Gardiner, M. H. Goldsmith, J. R. Hulance, D. M. Jackson, and J. B. Scattergood. Hierarchical compression for model-checking csp or how to check 1020 dining philosophers for deadlock. In Tools and Algorithms for the Construction and Analysis of Systems, pages 133-152, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. Google Scholar
  27. A.W. Roscoe. Theory and Practice of Concurrency. Prentice Hall, 1997. Google Scholar
  28. A.W. Roscoe. Understanding Concurrent Systems. Springer-Verlag, Berlin, Heidelberg, 1st edition, 2010. Google Scholar
  29. Dana Scott. Continuous lattices. In F. W. Lawvere, editor, Toposes, Algebraic Geometry and Logic, pages 97-136, Berlin, Heidelberg, 1972. Springer. Google Scholar
  30. Jun Sun, Yang Liu, Jin Song Dong, and Jun Pang. Pat: Towards flexible verification under fairness. In Ahmed Bouajjani and Oded Maler, editors, Computer Aided Verification, pages 709-714, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. Google Scholar
  31. Safouan Taha, Burkhart Wolff, and Lina Ye. The HOL-CSP refinement toolkit. Arch. Formal Proofs, 2020, 2020. URL: https://www.isa-afp.org/entries/CSP_RefTK.html.
  32. Safouan Taha, Burkhart Wolff, and Lina Ye. Philosophers may dine - definitively! In Brijesh Dongol and Elena Troubitsyna, editors, Integrated Formal Methods - 16th International Conference, IFM 2020, Lugano, Switzerland, November 16-20, 2020, Proceedings, volume 12546 of Lecture Notes in Computer Science, pages 419-439. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-63461-2_23.
  33. Safouan Taha, Lina Ye, and Burkhart Wolff. HOL-CSP Version 2.0. Archive of Formal Proofs, April 2019. URL: http://isa-afp.org/entries/HOL-CSP.html.
  34. Haykal Tej and Burkhart Wolff. A corrected failure divergence model for CSP in Isabelle/HOL. In John S. Fitzgerald, Cliff B. Jones, and Peter Lucas, editors, Formal Methods Europe (FME), volume 1313 of LNCS, pages 318-337. Springer, 1997. URL: https://doi.org/10.1007/3-540-63533-5_17.
  35. Jim Woodcock and Ana Cavalcanti. The semantics of circus. In Didier Bert, Jonathan P. Bowen, Martin C. Henson, and Ken Robinson, editors, ZB 2002: Formal Specification and Development in Z and B, 2nd International Conference of B and Z Users, Grenoble, France, January 23-25, 2002, Proceedings, volume 2272 of Lecture Notes in Computer Science, pages 184-203. Springer, 2002. URL: https://doi.org/10.1007/3-540-45648-1_10.
  36. Jim Woodcock, Ana Cavalcanti, Simon Foster, Marcel Oliveira, Augusto Sampaio, and Frank Zeyda. Utp, circus, and isabelle. In Jonathan P. Bowen, Qin Li, and Qiwen Xu, editors, Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 80th Birthday, volume 14080 of Lecture Notes in Computer Science, pages 19-51. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-40436-8_2.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact