Laboratory for Software Design

Got a question?

Got a question or comment? Contact us at (515) 294-6168 or hridesh@iastate.edu.

Automatic 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.

Bibliographic Information

@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},
}

Paper:[PDF]   Theorem2 Proof / Notes [PDF].