Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH scholarly article en Zhan, Bohua; Lv, Yi; Wang, Shuling; Zhao, Gehang; Hao, Jifeng; Ye, Hong; Xia, Bican https://www.dagstuhl.de/lipics License: Creative Commons Attribution 4.0 license (CC BY 4.0)
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-167420
URL:

; ; ; ; ; ;

Compositional Verification of Interacting Systems Using Event Monads

pdf-format:


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}
}

Keywords: Hoare Logic, Compositional Verification, Events
Seminar: 13th International Conference on Interactive Theorem Proving (ITP 2022)
Issue date: 2022
Date of publication: 03.08.2022
Supplementary Material: Software (Source Code): https://github.com/bzhan/EventSystem archived at: https://archive.softwareheritage.org/swh:1:dir:226d9c470f428a9e6c765fbea641d0b619b908cb


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI