Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL

Simon Foster, Chung-Kil Hur, Jim Woodcock

TL;DR

This article mechanise Interaction Trees (ITrees) in Isabelle/HOL to produce an execution and verification framework and demonstrates how ITrees can account for diverse semantic presentations, such as structural operational semantics, a relational program model, and CSP's failures-divergences trace model.

Abstract

Model execution allows us to prototype and analyse software engineering models by stepping through their possible behaviours, using techniques like animation and simulation. On the other hand, deductive verification allows us to construct formal proofs demonstrating satisfaction of certain critical properties in support of high-assurance software engineering. To ensure coherent results between execution and proof, we need unifying semantics and automation. In this paper, we mechanise Interaction Trees (ITrees) in Isabelle/HOL to produce an execution and verification framework. ITrees are coinductive structures that allow us to encode infinite labelled transition systems, yet they are inherently executable. We use ITrees to create verification tools for stateful imperative programs, concurrent programs with message passing in the form of the CSP and \Circus languages, and abstract system models in the style of the Z and B methods. We demonstrate how ITrees can account for diverse semantic presentations, such as structural operational semantics, a relational program model, and CSP's failures-divergences trace model. Finally, we demonstrate how ITrees can be executed using the Isabelle code generator to support the animation of models.

Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL

TL;DR

This article mechanise Interaction Trees (ITrees) in Isabelle/HOL to produce an execution and verification framework and demonstrates how ITrees can account for diverse semantic presentations, such as structural operational semantics, a relational program model, and CSP's failures-divergences trace model.

Abstract

Model execution allows us to prototype and analyse software engineering models by stepping through their possible behaviours, using techniques like animation and simulation. On the other hand, deductive verification allows us to construct formal proofs demonstrating satisfaction of certain critical properties in support of high-assurance software engineering. To ensure coherent results between execution and proof, we need unifying semantics and automation. In this paper, we mechanise Interaction Trees (ITrees) in Isabelle/HOL to produce an execution and verification framework. ITrees are coinductive structures that allow us to encode infinite labelled transition systems, yet they are inherently executable. We use ITrees to create verification tools for stateful imperative programs, concurrent programs with message passing in the form of the CSP and \Circus languages, and abstract system models in the style of the Z and B methods. We demonstrate how ITrees can account for diverse semantic presentations, such as structural operational semantics, a relational program model, and CSP's failures-divergences trace model. Finally, we demonstrate how ITrees can be executed using the Isabelle code generator to support the animation of models.
Paper Structure (25 sections, 21 theorems, 48 equations, 3 figures)

This paper contains 25 sections, 21 theorems, 48 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Notation
  3. Background
  4. Isabelle/HOL
  5. Circus and Z
  6. Interaction Trees and Operational Semantics
  7. Interaction Trees as Codatatypes
  8. ITree Combinators
  9. Structural Operational Semantics and Weak Bisimulation
  10. Iteration Chains
  11. Imperative Programs and Axiomatic Semantics
  12. Modelling Imperative Programs
  13. Concrete and Symbolic Execution
  14. Nondeterminism
  15. Predicative Semantics and Refinement
  16. ...and 10 more sections

Key Result

theorem 1

$$https://github.com/isabelle-utp/interaction-trees/blob/ff9f73f98c653b265bd9da55689715cf973499c1/Interaction_Trees.thy#L178

Figures (3)

  • Figure 1: An ITree fragment for the buffer example (approximate)
  • Figure 2: Animating the CSP buffer
  • Figure 3: Animating the Bounded Buffer Z-Machine

Theorems & Definitions (55)

  • definition 1: Interaction Tree Codatatype
  • definition 2: Divergent ITree
  • definition 3: Run ITree
  • definition 4: Interaction Tree Bind
  • theorem 1: Interaction Tree Bind Laws
  • theorem 2: ITree Coinduction
  • definition 5: Iteration
  • definition 6: Big-Step Operational Semantics
  • theorem 3: Transition Relation Properties
  • theorem 4: Sequential Operational Semantics
  • ...and 45 more