Document Open Access Logo

Compositional Verification of Interacting Systems Using Event Monads

Authors Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, Bican Xia

PDF
Thumbnail PDF

File

LIPIcs.ITP.2022.33.pdf
  • Filesize: 0.64 MB
  • 21 pages

Document Identifiers

Author Details

Bohua Zhan
  • State Key Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
Yi Lv
  • State Key Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
Shuling Wang
  • State Key Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
Gehang Zhao
  • School of Mathematical Sciences, Peking University, Beijing, China
Jifeng Hao
  • Aeronautics Computing Technique Research Institute, Xi'an, China
Hong Ye
  • Aeronautics Computing Technique Research Institute, Xi'an, China
Bican Xia
  • School of Mathematical Sciences, Peking University, Beijing, China

Funding

This work was partially supported by the National Natural Science Foundation of China under Grant Nos. 61732001, 62002351, 62032024, 61972385.

Cite AsGet BibTex

Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, and Bican Xia. Compositional Verification of Interacting Systems Using Event Monads. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ITP.2022.33

Abstract

Large software systems are usually divided into multiple components that interact with each other. How to verify interacting components in a modular way is one of the major problems in formal verification. In many cases, interaction between components can be modeled asynchronously, where events are sent without requiring a response in order to continue with execution of the component. In this paper, we propose a lightweight, event-based framework for verification of components with asynchronous interaction. We define event monads and event systems, and a Hoare logic-style calculus for reasoning about them. The framework is implemented in Isabelle and applied to several case studies, including models for distributed computing, cache-coherence protocols, and verification of partition scheduling in a real-time operating system.

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • Hoare Logic
  • Compositional Verification
  • Events

Metrics

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

Supplementary Materials

References

  1. Martín Abadi and Leslie Lamport. Composing specifications. ACM Trans. Program. Lang. Syst., 15(1):73-132, 1993. Google Scholar
  2. Aeronautical Radio Inc. ARINC Specification 653: Avionics Application Software Standard Interface, Part 1-Required Services. ARINC Airlines Electronic Engineering Committee, 2015. Google Scholar
  3. Danel Ahman and Matija Pretnar. Asynchronous effects. Proc. ACM Program. Lang., 5(POPL):1-28, 2021. Google Scholar
  4. Andrej Bauer and Matija Pretnar. Programming with algebraic effects and handlers. J. Log. Algebraic Methods Program., 84(1):108-123, 2015. URL: https://doi.org/10.1016/j.jlamp.2014.02.001.
  5. Zhou Chaochen, C. A. R. Hoare, and Anders P. Ravn. A calculus of durations. Inf. Process. Lett., 40(5):269-276, 1991. URL: https://doi.org/10.1016/0020-0190(91)90122-X.
  6. Ching-Tsun Chou, Phanindra K. Mannava, and Seungjoon Park. A simple method for parameterized verification of cache coherence protocols. In Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings, pages 382-398, 2004. Google Scholar
  7. David Cock, Gerwin Klein, and Thomas Sewell. Secure microkernels, state monads and scalable refinement. In Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, pages 167-182, 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_16.
  8. Jeffrey Dean and Sanjay Ghemawat. MapReduce: simplified data processing on large clusters. Commun. ACM, 51(1):107-113, 2008. Google Scholar
  9. Simon Foster. Hybrid relations in isabelle/utp. In Unifying Theories of Programming - 7th International Symposium, UTP 2019, Dedicated to Tony Hoare on the Occasion of His 85th Birthday, Porto, Portugal, October 8, 2019, Proceedings, pages 130-153, 2019. Google Scholar
  10. Simon Foster, James Baxter, Ana Cavalcanti, Alvaro Miyazawa, and Jim Woodcock. Automating verification of state machines with reactive designs and isabelle/utp. In Formal Aspects of Component Software - 15th International Conference, FACS 2018, Pohang, South Korea, October 10-12, 2018, Proceedings, pages 137-155, 2018. Google Scholar
  11. Simon Foster, James Baxter, Ana Cavalcanti, Jim Woodcock, and Frank Zeyda. Unifying semantic foundations for automated verification tools in Isabelle/UTP. Sci. Comput. Program., 197:102510, 2020. Google Scholar
  12. David Greenaway. Automated proof-producing abstraction of C code. PhD thesis, University of New South Wales, Sydney, Australia, 2014. URL: http://handle.unsw.edu.au/1959.4/54260.
  13. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. Certikos: An extensible architecture for building certified concurrent OS kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016, pages 653-669, 2016. URL: https://www.usenix.org/conference/osdi16/technical-sessions/presentation/gu.
  14. Xiaojie Guo, Maxime Lesourd, Mengqi Liu, Lionel Rieg, and Zhong Shao. Integrating formal schedulability analysis into a verified OS kernel. In Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II, pages 496-514, 2019. URL: https://doi.org/10.1007/978-3-030-25543-5_28.
  15. Joseph Y. Halpern, Zohar Manna, and Ben C. Moszkowski. A hardware semantics based on temporal intervals. In Automata, Languages and Programming, 10th Colloquium, Barcelona, Spain, July 18-22, 1983, Proceedings, pages 278-291, 1983. URL: https://doi.org/10.1007/BFb0036915.
  16. Maximilian P. L. Haslbeck and Peter Lammich. For a few dollars more - verified fine-grained algorithm analysis down to LLVM. In Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, pages 292-319, 2021. Google Scholar
  17. C.A.R Hoare and Jifeng He. Unifying Theories of Programming. Prentice-Hall, 1998. Google Scholar
  18. Gerwin Klein. Operating system verification-an overview. Sadhana, 34:27-69, 2009. Google Scholar
  19. Gerwin Klein, June Andronick, Kevin Elphinstone, Toby C. Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst., 32(1):2:1-2:70, 2014. URL: https://doi.org/10.1145/2560537.
  20. Jérémie Koenig and Zhong Shao. Refinement-based game semantics for certified abstraction layers. In LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 633-647, 2020. URL: https://doi.org/10.1145/3373718.3394799.
  21. 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 Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pages 234-248, 2019. URL: https://doi.org/10.1145/3293880.3294106.
  22. Peter Lammich. Refinement to imperative HOL. J. Autom. Reason., 62(4):481-503, 2019. Google Scholar
  23. Peter Lammich and Thomas Tuerk. Applying data refinement for monadic programs to hopcroft’s algorithm. In Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings, pages 166-182, 2012. Google Scholar
  24. Thomas Letan, Yann Régis-Gianas, Pierre Chifflier, and Guillaume Hiet. Modular verification of programs with effects and effects handlers. Formal Aspects Comput., 33(1):127-150, 2021. URL: https://doi.org/10.1007/s00165-020-00523-2.
  25. Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, and Man-Ki Yoon. Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation. Proc. ACM Program. Lang., 4(POPL):20:1-20:31, 2020. URL: https://doi.org/10.1145/3371088.
  26. Nancy A. Lynch and Eugene W. Stark. A proof of the Kahn principle for input/output automata. Inf. Comput., 82(1):81-92, 1989. URL: https://doi.org/10.1016/0890-5401(89)90066-7.
  27. Nancy A. Lynch and Mark R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, Vancouver, British Columbia, Canada, August 10-12, 1987, pages 137-151, 1987. URL: https://doi.org/10.1145/41840.41852.
  28. Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, and Gerwin Klein. sel4: From general purpose to a proof of information flow enforcement. In 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19-22, 2013, pages 415-429, 2013. Google Scholar
  29. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  30. Gordon D. Plotkin and Matija Pretnar. Handlers of algebraic effects. In Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, York, UK, March 22-29, 2009. Proceedings, pages 80-94, 2009. URL: https://doi.org/10.1007/978-3-642-00590-9_7.
  31. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pages 55-74, 2002. URL: https://doi.org/10.1109/LICS.2002.1029817.
  32. Frédéric Tuong and Burkhart Wolff. Clean - an abstract imperative programming language and its theory. Arch. Formal Proofs, 2019, 2019. URL: https://www.isa-afp.org/entries/Clean.html.
  33. Freek Verbeek, Oto Havle, Julien Schmaltz, Sergey Tverdyshev, Holger Blasum, Bruno Langenstein, Werner Stephan, Burkhart Wolff, and Yakoub Nemouchi. Formal API specification of the pikeos separation kernel. In NASA Formal Methods - 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings, pages 375-389, 2015. Google Scholar
  34. Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang., 4(POPL):51:1-51:32, 2020. URL: https://doi.org/10.1145/3371119.
  35. Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang, and Zhaohui Li. A practical verification framework for preemptive OS kernels. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, pages 59-79, 2016. URL: https://doi.org/10.1007/978-3-319-41540-6_4.
  36. 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 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference), pages 32:1-32:19, 2021. Google Scholar
  37. Yongwang Zhao and David Sanán. Rely-guarantee reasoning about concurrent memory management in Zephyr RTOS. In Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II, pages 515-533, 2019. URL: https://doi.org/10.1007/978-3-030-25543-5_29.
  38. Yongwang Zhao, David Sanán, Fuyuan Zhang, and Yang Liu. Reasoning about information flow security of separation kernels with channel-based communication. In Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, pages 791-810, 2016. Google Scholar
  39. Yongwang Zhao, David Sanán, Fuyuan Zhang, and Yang Liu. A parametric rely-guarantee reasoning framework for concurrent reactive systems. In Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings, pages 161-178, 2019. URL: https://doi.org/10.1007/978-3-030-30942-8_11.
  40. Yongwang Zhao, Zhibin Yang, and Dianfu Ma. A survey on formal specification and verification of separation kernels. Frontiers Comput. Sci., 11(4):585-607, 2017. URL: https://doi.org/10.1007/s11704-016-4226-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