Golok: Push-button Verification of Parameterized Systems

Thumbnail Image
Date
2011-01-23
Authors
Hanna, Youssef
Samuelson, David
Basu, Samik
Rajan, Hridesh
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Authors
Person
Rajan, Hridesh
Professor and Department Chair of Computer Science
Research Projects
Organizational Units
Organizational Unit
Journal Issue
Is Version Of
Versions
Series
Department
Computer Science
Abstract

Parameterized systems verification is a long-standing problem, where the challenge is to verify that a property holds for all (infinite) instances of the parameterized system. Existing techniques aim to reduce this problem to checking the properties on smaller systems with a bound on the parameter referred to as the "cut-off" such that if the property holds for system instances of size cut-off that implies that it holds for larger system instances. In most existing techniques, human guidance is required to deduce the invariants for the system's behavior, which are then used to compute cut-off. In contrast, we present an fully automatic sound method (but necessarily incomplete) for generating the cut-off that works for synchronous parameterized systems with heterogeneous processes communicating via single-cast and/or broadcast. Our technique is independent of the system topology and the property to be verified. Given the specification and the topology of the system, our technique generates the system-specific cut-off. We have realized our technique in a tool, Golok, which shows that it can be automated. We present the results of running Golok on 15 parameterized systems where we obtain smaller cut-offs than those presented in the existing literature for 14 cases.

Comments

Copyright © 2011, Youssef Hanna, David Samuelson, Samik Basu, Hridesh Rajan. All rights reserved.

Description
Keywords
Citation
DOI
Source
Subject Categories
Copyright
Collections