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

Simon Foster; Chung-Kil Hur; Jim Woodcock

doi:10.4230/LIPIcs.CONCUR.2021.20

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

Simon Foster, Chung-Kil Hur, Jim Woodcock

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	International Conference on Concurrency Theory (CONCUR 2021)
Publisher	Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany
DOIs	https://doi.org/10.4230/LIPIcs.CONCUR.2021.20
Publication status	Published - 13 Aug 2021

Publication series

Name	LIPIcs
ISSN (Electronic)	1868-8969

Bibliographical note

14 pages, submitted to CONCUR 2021

Keywords

cs.LO

Access to Document

10.4230/LIPIcs.CONCUR.2021.20Licence: CC BY

LIPIcs-CONCUR-2021-20Final published version, 941 KBLicence: CC BY

Cite this

@inproceedings{cd5ef6ff84784aada4044ce302046e7c,

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. ",

keywords = "cs.LO",

author = "Simon Foster and Chung-Kil Hur and Jim Woodcock",

note = "14 pages, submitted to CONCUR 2021",

year = "2021",

month = aug,

day = "13",

doi = "10.4230/LIPIcs.CONCUR.2021.20",

language = "English",

series = "LIPIcs",

publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik, Germany",

booktitle = "International Conference on Concurrency Theory (CONCUR 2021)",

}

Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL. / Foster, Simon; Hur, Chung-Kil; Woodcock, Jim.
International Conference on Concurrency Theory (CONCUR 2021). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, 2021. (LIPIcs).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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

AU - Foster, Simon

AU - Hur, Chung-Kil

AU - Woodcock, Jim

N1 - 14 pages, submitted to CONCUR 2021

PY - 2021/8/13

Y1 - 2021/8/13

N2 - 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.

AB - 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.

KW - cs.LO

U2 - 10.4230/LIPIcs.CONCUR.2021.20

DO - 10.4230/LIPIcs.CONCUR.2021.20

M3 - Conference contribution

T3 - LIPIcs

BT - International Conference on Concurrency Theory (CONCUR 2021)

PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany

ER -