Golok: Push-button Verification of Parameterized Systems

Date
2011-01-23
Authors
Hanna, Youssef
Samuelson, David
Basu, Samik
Rajan, Hridesh
Journal Title
Journal ISSN
Volume Title
Publisher
Altmetrics
Authors
Research Projects
Organizational Units
Computer Science
Organizational Unit
Journal Issue
Series
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.

Description

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

Keywords
paramterized model checking, behavioral automaton, composition
Citation
DOI
Source
Collections