利用反应式设计与 Isabelle/UTP 自动验证状态机
计算机科学中的逻辑
2018-10-11 v2
摘要
基于状态机的表示法在组件系统（尤其是机器人领域）的描述中无处不在。为确保这些系统安全且可预测，形式化验证技术十分重要，且若其兼具自动化与可扩展性则具成本效益。本文中，我们提出一种针对图示化状态机语言的验证方法，其利用定理证明与基于统一编程理论（UTP）的指称语义。我们提供必要的理论以支撑状态机（包括迭代过程的归纳定理），将用于状态与迁移的动作语言机械化，并用以形式化语义。随后我们描述该验证方法，其支持无限状态系统，并以一个完全自动化的死锁自由性检查为例示之。该工作已在我们的证明工具 Isabelle/UTP 中机械化，因而也展示了利用 UTP 构建实用验证工具的方法。
引用
@article{arxiv.1807.08588,
title = {Automating Verification of State Machines with Reactive Designs and Isabelle/UTP},
author = {Simon Foster and James Baxter and Ana Cavalcanti and Alvaro Miyazawa and Jim Woodcock},
journal= {arXiv preprint arXiv:1807.08588},
year = {2018}
}
备注
18 pages, 16th Intl. Conf. on Formal Aspects of Component Software (FACS 2018), October 2018, Pohang, South Korea