Automating Cut-off for Multi-parameterized Systems

PDF Download Download Paper Theorem 2

Abstract

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 multi-parameterized 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.

Bib Info


@InProceedings{hanna10a,
  author = {Youssef Hanna and David Samuelson and Samik Basu and Hridesh Rajan},
  title = {Automating Cut-off for Multi-parameterized Systems},
  booktitle = {The 12th International Conference on Formal Engineering Methods (ICFEM 2010)},
  year = {2010},
  month = {November},
  address = {Shanghai, China},
}