Document Open Access Logo

Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL

Authors Simon Foster , Chung-Kil Hur, Jim Woodcock

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2021.20.pdf
  • Filesize: 0.91 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
Keywords
  • Coinduction
  • Process Algebra
  • Theorem Proving
  • Simulation

Metrics

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

Abstract

Simulation and formal verification are important complementary techniques necessary in high assurance model-based systems development. In order to support coherent results, it is necessary to provide unifying semantics and automation for both activities. In this paper we apply Interaction Trees in Isabelle/HOL to produce a verification and simulation framework for state-rich process languages. We develop the core theory and verification techniques for Interaction Trees, use them to give a semantics to the CSP and Circus languages, and formally link our new semantics with the failures-divergences semantic model. We also show how the Isabelle code generator can be used to generate verified executable simulations for reactive and concurrent programs.

Cite As Get BibTex

Simon Foster, Chung-Kil Hur, and Jim Woodcock. Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CONCUR.2021.20

Author Details

Simon Foster
  • University of York, UK
Chung-Kil Hur
  • Seoul National University, South Korea
Jim Woodcock
  • University of York, UK

Funding

  • Foster, Simon: EPSRC EP/S001190/1 (CyPhyAssure).
  • Woodcock, Jim: EPSRC EP/V026801/1 (TAS Verifiability), EP/M025756/1 (RoboCalc).

Acknowledgements

We would like to thank the anonymous reviewers of our paper, whose helpful and insightful comments have improved the content and presentation.

Supplementary Materials

References

  1. R.-J. Back and J. Wright. Refinement Calculus: A Systematic Introduction. Springer, 1998. Google Scholar
  2. J. Baxter, P. Ribeiro, and A. Cavalcanti. Sound reasoning in tock-CSP. Acta Informatica, April 2021. URL: https://doi.org/10.1007/s00236-020-00394-3.
  3. J. C. Blanchette, A. Bouzy, A. Lochbihler, A. Popescu, and D. Traytel. Friends with Benefits: Implementing Corecursion in Foundational Proof Assistants. In Programming Languages and Systems, 26th European Symposium on Programming (ESOP), 2017. Google Scholar
  4. J. C. Blanchette, J. Hölzl, A. Lochbihler, L. Panny, A. Popescu, and D. Traytel. Truly modular (co)datatypes for Isabelle/HOL. In Gerwin Klein and Ruben Gamboa, editors, 5th Intl. Conf. on Interactive Theorem Proving (ITP), volume 8558 of LNCS, pages 93-110. Springer, 2014. Google Scholar
  5. J. C. Blanchette, C. Kaliszyk, L. C. Paulson, and J. Urban. Hammering towards QED. Journal of Formalized Reasoning, 9(1), 2016. URL: https://doi.org/10.6092/issn.1972-5787/4593.
  6. J. C. Blanchette, A. Popescu, and D. Traytel. Foundational extensible corecursion: a proof assistant perspective. In 20th Intl. Conf. on Functional Programming (ICFP), pages 192-204. ACM, August 2015. URL: https://doi.org/10.1145/2858949.2784732.
  7. J. C. Blanchette, A. Popescu, and D. Traytel. Soundness and completeness proofs by coinductive methods. Journal of Automated Reasoning, 58:149-179, 2017. URL: https://doi.org/10.1007/s10817-016-9391-3.
  8. S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential processes. Journal of the ACM, 31(3):560-599, 1984. URL: https://doi.org/10.1145/828.833.
  9. A. Cavalcanti, A. Sampaio, A. Miyazawa, P. Ribeiro, M. Filho, A. Didier, W. Li, and J. Timmis. Verified simulation for robotics. Science of Computer Programming, 174:1-37, 2019. URL: https://doi.org/10.1016/j.scico.2019.01.004.
  10. J. Ferlez, R. Cleaveland, and S. Marcus. Generalized synchronization trees. In Proc. 17th Intl. Conf. on Foundations of Software Science and Computation Structures (FOSSACS), volume 8412 of LNCS, pages 304-319. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54830-7_20.
  11. J. Ferlez, R. Cleaveland, and S. I. Marcus. Bisimulation in behavioral dynamical systems and generalized synchronization trees. In Proc. 2018 IEEE Conf. on Decision and Control (CDC), pages 751-758. IEEE, 2018. URL: https://doi.org/10.1109/CDC.2018.8619607.
  12. J. Foster. Bidirectional programming languages. PhD thesis, University of Pennsylvania, 2009. Google Scholar
  13. S. Foster. Hybrid relations in Isabelle/UTP. In 7th Intl. Symp. on Unifying Theories of Programming (UTP), volume 11885 of LNCS, pages 130-153. Springer, 2019. Google Scholar
  14. S. Foster, J. Baxter, A. Cavalcanti, J. Woodcock, and F. Zeyda. Unifying semantic foundations for automated verification tools in Isabelle/UTP. Science of Computer Programming, 197, October 2020. URL: https://doi.org/10.1016/j.scico.2020.102510.
  15. S. Foster, A. Cavalcanti, S. Canham, J. Woodcock, and F. Zeyda. Unifying theories of reactive design contracts. Theoretical Computer Science, 802:105-140, January 2020. URL: https://doi.org/10.1016/j.tcs.2019.09.017.
  16. S. Foster, K. Ye, A. Cavalcanti, and J. Woodcock. Automated verification of reactive and concurrent programs by calculation. Journal of Logical and Algebraic Methods in Programming, 121, June 2021. URL: https://doi.org/10.1016/j.jlamp.2021.100681.
  17. T. Gibson-Robinson, P. Armstrong, A. Boulgakov, and A. W. Roscoe. FDR3 - A Modern Refinement Checker for CSP. In Erika Ábrahám and Klaus Havelund, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 8413 of LNCS, pages 187-201, 2014. Google Scholar
  18. F. Haftmann, A. Krauss, O. Kuncar, and T. Nipkow. Data refinement in Isabelle/HOL. In Proc. 4th Intl. Conf. on Interactive Theorem Proving (ITP), volume 7998 of LNCS, pages 100-115. Springer, 2013. Google Scholar
  19. F. Haftmann and T. Nipkow. Code generation via higher-order rewrite systems. In 10th Intl. Symp. on Functional and Logic Programming (FLOPS), volume 6009 of LNCS, pages 103-117. Springer, 2010. Google Scholar
  20. Matthew Hennessy and Tim Regan. A process algebra for timed systems. Information and Computation, 117(2):221-239, 1995. Google Scholar
  21. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985. Google Scholar
  22. C. A. R. Hoare, I. Hayes, J. He, C. Morgan, A. Roscoe, J. Sanders, I. Sørensen, J. Spivey, and B. Sufrin. The laws of programming. Communications of the ACM, 30(8):672-687, August 1987. Google Scholar
  23. Nicolas Koh, Yao Li, Yishuai Li, Li yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic. From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server. In Proc. 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), 2019. URL: https://doi.org/10.1145/3293880.3294106.
  24. M. Leuschel and M. Butler. ProB: an automated analysis toolset for the B method. Int J Softw Tools Technol Transf, 10:185-203, 2008. URL: https://doi.org/10.1007/s10009-007-0063-9.
  25. Yishuai Li, Benjamin C. Pierce, and Steve Zdancewic. Model-based testing of networked applications. In Proc. 30th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), 2021. Google Scholar
  26. William Mansky, Wolf Honoré, and Andrew W. Appel. Connecting higher-order separation logic to a first-order outside world. In Proc. 29th European Symposium on Programming (ESOP), 2020. Google Scholar
  27. Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980. Google Scholar
  28. Robin Milner. Communication and Concurrency. Prentice Hall, 1989. Google Scholar
  29. A. Miyazawa, P. Ribeiro, W. Li, A. Cavalcanti, J. Timmis, and J. Woodcock. RoboChart: modelling and verification of the functional behaviour of robotic applications. Software and Systems Modelling, January 2019. URL: https://doi.org/10.1007/s10270-018-00710-z.
  30. C. Morgan. Programming from Specifications. Prentice-Hall, January 1996. Google Scholar
  31. J. H. Y. Munive, G. Struth, and S. Foster. Differential Hoare logics and refinement calculi for hybrid systems with Isabelle/HOL. In RAMiCS, volume 12062 of LNCS. Springer, April 2020. URL: https://doi.org/10.1007/978-3-030-43520-2_11.
  32. M. Oliveira, A. Cavalcanti, and J. Woodcock. A UTP semantics for Circus. Formal Aspects of Computing, 21:3-32, 2009. URL: https://doi.org/10.1007/s00165-007-0052-5.
  33. M. Pickering, J. Gibbons, and N. Wu. Profunctor optics: Modular data accessors. The Art, Science, and Engineering of Programming, 1(2), 2017. URL: https://doi.org/10.22152/programming-journal.org/2017/1/7.
  34. A. W. Roscoe. Denotational semantics for Occam. In Intl. Seminar on Concurrency, volume 197 of LNCS, pages 306-329. Springer, 1984. Google Scholar
  35. A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 2005. Google Scholar
  36. A. W. Roscoe. Understanding Concurrent Systems. Springer, 2010. Google Scholar
  37. Lucas Silver and Steve Zdancewic. Dijkstra monads forever: Termination-sensitive specifications for Interaction Trees. Proceedings of the ACM on Programming Languages, 5(POPL), January 2021. URL: https://doi.org/10.1145/3434307.
  38. M. Spivey. The Z-Notation - A Reference Manual. Prentice Hall, Englewood Cliffs, N. J., 1989. Google Scholar
  39. S. Taha, B. Wolff, and L. Ye. Philosophers may dine - definitively! In Proc. 16th Intl. Conf. on Integrated Formal Methods, LNCS. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-63461-2_23.
  40. R. J. van Glabbeek. Notes on the methodology of CCS and CSP. Theoretical Computer Science, 1997. Google Scholar
  41. G. Winsel. Synchronisation trees. Theoretical Computer Science, 34(1-2):33-82, 1984. Google Scholar
  42. J. Woodcock and A. Cavalcanti. A concurrent language for refinement. In A. Butterfield, G. Strong, and C. Pahl, editors, Proc. 5th Irish Workshop on Formal Methods (IWFM), Workshops in Computing. BCS, July 2001. Google Scholar
  43. L.-Y. Xia, Y. Zakowski, P. He, C.-K. Hur, G. Malecha, B. C. Pierce, and S. Zdancewic. Interaction trees: Representing recursive and impure programs in Coq. In Proc. 47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM, 2020. URL: https://doi.org/10.1145/3371119.
  44. Yannick Zakowski, Paul He, Chung-Kil Hur, and Steve Zdancewic. An equational theory for weak bisimulation via generalized parameterized coinduction. In Proc. 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), 2020. URL: https://doi.org/10.1145/3372885.3373813.
  45. Vadim Zaliva, Ilia Zaichuk, and Franz Franchetti. Verified translation between purely functional and imperative domain specific languages in HELIX. In Proc. 12th International Conference on Verified Software: Theories, Tools, Experiments (VSTTE), 2020. Google Scholar
  46. Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, and Steve Zdancewic. Verifying an HTTP key-value server with Interaction Trees and VST. In Proc. 12th International Conference on Interactive Theorem Proving (ITP), 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.32.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact