Automating Cut-off for Multi-parameterized Systems
Automating Cut-off for Multi-parameterized Systems
复制标题
多参数化系统的自动切断
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Hridesh Rajan
中科院分区：
文献类型：
--
作者：
Youssef Hanna;David Samuelson;Samik Basu;Hridesh Rajan
验证参数化系统满足某些所需的属性，以验证系统实例的无限家族。总体而言，这个问题是不确定的，因此已经提出了许多声音和不完整的技术来解决它。现有技术通常集中于具有单个参数的参数化系统（即，恰好一种类型的过程数量取决于参数的系统）；但是，实践中的许多系统都是多参数化的，其中使用多个参数来指定系统中不同类型的过程的数量。在这项工作中，我们提出了一种针对多聚体系统的自动验证技术，证明其健全性并表明它可以应用于系统，而与其通信拓扑无关。我们在工具Golok中介绍了我们技术的原型实现，并使用许多多参数化系统证明了其实际适用性。
Verifying that a parameterized system satisfies certain desired properties amounts to verifying an infinite family of the system instances. This problem is undecidable in general, and as such a number of sound and incomplete techniques have been proposed to address it. Existing techniques typically focus on parameterized systems with a single parameter, (i.e., on systems where the number of processes of exactly one type is dependent on the parameter); however, many systems in practice are multi-parameterized, where multiple parameters are used to specify the number of different types of processes in the system. In this work, we present an automatic verification technique for multiparameterized systems, prove its soundness and show that it can be applied to systems irrespective of their communication topology. We present a prototype realization of our technique in our tool Golok, and demonstrate its practical applicability using a number of multi-parameterized systems.