Paper Info
Title
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.
Year
DOI
Venue
2021
10.4230/LIPIcs.CONCUR.2021.20
CONCUR
DocType
Citations 
PageRank 
Conference
0
0.34
References 
Authors
0
3
Name
Order
Citations
PageRank
Simon Foster16313.44
Chung-Kil Hur200.34
Jim Woodcock353477.08