基于反应式设计和Isabelle/UTP的状态机自动验证
Automating Verification of State Machines with Reactive Designs and Isabelle/UTP
摘要：
基于状态机的符号在组件系统的描述中无处不在，特别是在机器人领域。为了确保这些系统的安全性和可预测性，形式化验证技术是重要的，如果它们是自动化和可扩展的，则可以具有成本效益。在本文中，我们提出了一个验证方法的图形状态机语言，利用定理证明和指称语义的基础上统一编程理论（UTP）。我们提供了必要的理论来支撑状态机（包括迭代过程的归纳定理），机械化状态和转换的动作语言，并使用这些来形式化语义。然后，我们描述的验证方法，它支持无限状态系统，并使用一个完全自动化的死锁自由检查。这项工作已经在我们的证明工具Isabelle/UTP中实现了机械化，因此也说明了使用UTP来构建实用的验证工具。
英文摘要：
State-machine based notations are ubiquitous in the description of component systems, particularly in the robotic domain. To ensure these systems are safe and predictable, formal verification techniques are important, and can be cost-effective if they are both automated and scalable. In this paper, we present a verification approach for a diagrammatic state machine language that utilises theorem proving and a denotational semantics based on Unifying Theories of Programming (UTP). We provide the necessary theory to underpin state machines (including induction theorems for iterative processes), mechanise an action language for states and transitions, and use these to formalise the semantics. We then describe the verification approach, which supports infinite state systems, and exemplify it with a fully automated deadlock-freedom check. The work has been mechanised in our proof tool, Isabelle/UTP, and so also illustrates the use of UTP to build practical verification tools.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
