License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2022.33
URN: urn:nbn:de:0030-drops-167420
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16742/
Zhan, Bohua ;
Lv, Yi ;
Wang, Shuling ;
Zhao, Gehang ;
Hao, Jifeng ;
Ye, Hong ;
Xia, Bican
Compositional Verification of Interacting Systems Using Event Monads
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.
BibTeX - Entry
@InProceedings{zhan_et_al:LIPIcs.ITP.2022.33,
author = {Zhan, Bohua and Lv, Yi and Wang, Shuling and Zhao, Gehang and Hao, Jifeng and Ye, Hong and Xia, Bican},
title = {{Compositional Verification of Interacting Systems Using Event Monads}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {33:1--33:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16742},
URN = {urn:nbn:de:0030-drops-167420},
doi = {10.4230/LIPIcs.ITP.2022.33},
annote = {Keywords: Hoare Logic, Compositional Verification, Events}
}
