Automating Cut-off for Multi-parameterized Systems

By: Youssef Hanna, David Samuelson, Samik Basu, and Hridesh Rajan

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.

ACM Reference

Hanna, Y. et al. 2010. Automating Cut-off for Multi-parameterized Systems. Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM, Shanghai, China (2010), 338–354.

BibTeX Reference

@inproceedings{HannaSamuelsonBasuRajan2010,
  author = {Youssef Hanna and David Samuelson and Samik Basu and Hridesh Rajan},
  title = {Automating Cut-off for Multi-parameterized Systems},
  booktitle = {Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM, Shanghai, China},
  volume = {6447},
  series = {Lecture Notes in Computer Science},
  pages = {338--354},
  year = {2010},
  publisher = {Springer},
  editor = {Jin Song Dong and Huibiao Zhu},
  doi = {10.1007/978-3-642-16901-4\_23},
  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.},
}