论文标题
通过计算对反应性和并发程序的自动验证
Automated Verification of Reactive and Concurrent Programs by Calculation
论文作者
论文摘要
反应性程序将传统的顺序编程结构与原始构造相结合，以允许与其他并发代理进行通信。它们在现代应用程序中无处不在，从组件系统和Web服务到网络物理系统和自主机器人。在本文中，我们提出了具有较大或无限状态空间的并发反应性程序的代数验证策略。我们定义新型操作员来表征相互作用和状态更新，以及相关的方程理论。因此，我们可以计算一个反应性程序的表示语义，从而促进自动证明。值得注意的是，我们对基于Kleene代数的反应性不变的迭代程序的推理支持以及平行组成。我们通过验证反应性缓冲液来说明我们的策略。我们的法律和策略是在伊莎贝尔/UTP的机械化的，我们对Hoare的实施，他统一了编程理论（UTP）框架，以提供合理的保证和实际验证支持。
Reactive programs combine traditional sequential programming constructs with primitives to allow communication with other concurrent agents. They are ubiquitous in modern applications, ranging from components systems and web services, to cyber-physical systems and autonomous robots. In this paper, we present an algebraic verification strategy for concurrent reactive programs, with a large or infinite state space. We define novel operators to characterise interactions and state updates, and an associated equational theory. With this we can calculate a reactive program's denotational semantics, and thereby facilitate automated proof. Of note is our reasoning support for iterative programs with reactive invariants, based on Kleene algebra, and for parallel composition. We illustrate our strategy by verifying a reactive buffer. Our laws and strategy are mechanised in Isabelle/UTP, our implementation of Hoare and He's Unifying Theories of Programming (UTP) framework, to provide soundness guarantees and practical verification support.
