基于 Isabelle/HOL 中交互树的状态丰富过程的形式化验证仿真
计算机科学中的逻辑
2021-05-12 v1
摘要
仿真与形式化验证是基于模型的系统高可信开发中重要且互补的技术。为支持连贯的结果，有必要为这两项活动提供统一的语义与自动化。本文在 Isabelle/HOL 中应用交互树（Interaction Trees），为状态丰富的过程语言构建一个验证与仿真框架。我们发展了交互树的核心理论与验证技术，用其为 CSP 与 Circus 语言给出语义，并将新语义与失败-发散语义模型形式化关联。我们还展示了如何利用 Isabelle 代码生成器为反应式与并发程序生成经验证的可执行仿真。
引用
@article{arxiv.2105.05133,
title = {Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL},
author = {Simon Foster and Chung-Kil Hur and Jim Woodcock},
journal= {arXiv preprint arXiv:2105.05133},
year = {2021}
}
备注
14 pages, submitted to CONCUR 2021