论文标题
验证归纳定义的参数化系统的安全性能
Verifying Safety Properties of Inductively Defined Parameterized Systems
论文作者
论文摘要
我们将术语代数作为一种新的正式规范语言，用于通过有限但无限数量的组件组成的分布式系统的协调架构。该语言允许描述一组无限的系统，其组件之间的协调共享相同的模式，使用归纳定义，类似于用于描述代数数据类型或递归数据结构的系统。此外，我们依赖于能够证明一般安全性能的结构不变性的自动综合（相互排斥，缺乏僵局）的结构不变性的自动合成，为本语言中描述的参数系统提供了验证方法。使用Monadic二阶逻辑的WSK片段定义了不变性，已知可以通过经典的自动机 - 逻辑连接来确定。这将安全验证问题减少到检查WSK公式的满意度。
We introduce a term algebra as a new formal specification language for the coordinating architectures of distributed systems consisting of a finite yet unbounded number of components. The language allows to describe infinite sets of systems whose coordination between components share the same pattern, using inductive definitions similar to the ones used to describe algebraic data types or recursive data structures. Further, we give a verification method for the parametric systems described in this language, relying on the automatic synthesis of structural invariants that enable proving general safety properties (mutual exclusion, absence of deadlocks). The invariants are defined using the WSkS fragment of the monadic second order logic, known to be decidable by a classical automata-logic connection. This reduces the safety verification problem to checking satisfiability of a WSkS formula.
