archives

Golok: Push-button Verification of Parameterized Systems


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Hanna, Youssef, Samuelson, David, Basu, Samik and Rajan, Hridesh (2011) Golok: Push-button Verification of Parameterized Systems. Technical Report 11-02, Computer Science, Iowa State University.

Full text available as:Adobe PDF

This is the latest version of this eprint.

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.

Subjects:Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)
ID code:00000659
Deposited by:Youssef Hanna on 29 March 2011

Available Versions of This Paper



Contact site administrator at: ssg@cs.iastate.edu