Automating Cut-off for Multi-parameterized Systems

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.

• Type: Journal
• Year: 2010
• Where: ICFEM
• Authors: Youssef Hanna, David Samuelson, Samik Basu, Hridesh Rajan
• Keywords: Certain Desired Properties, ICFEM 2010, Parameters, Software Engineering, Systems