Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL

TL;DR

This paper introduces a framework using Interaction Trees in Isabelle/HOL for the formal verification and simulation of state-rich process languages, unifying semantics and automation.

Contribution

It develops core theory and verification techniques for Interaction Trees, providing a formal semantics for CSP and Circus, and links them with existing semantic models.

Findings

Verified executable simulations for reactive programs

Formal semantics for CSP and Circus languages

Linking new semantics with failures-divergences model

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.