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.CONCUR.2021.20
URN: urn:nbn:de:0030-drops-143973
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14397/
Foster, Simon ;
Hur, Chung-Kil ;
Woodcock, Jim
Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL
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.
BibTeX - Entry
@InProceedings{foster_et_al:LIPIcs.CONCUR.2021.20,
author = {Foster, Simon and Hur, Chung-Kil and Woodcock, Jim},
title = {{Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {20:1--20:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/14397},
URN = {urn:nbn:de:0030-drops-143973},
doi = {10.4230/LIPIcs.CONCUR.2021.20},
annote = {Keywords: Coinduction, Process Algebra, Theorem Proving, Simulation}
}
