Golok: Push-button Verification of Parameterized Systems


These pages describe work carried out under the Golok project. The PIs are Hridesh Rajan and Samik Basu and much of the work is carried out by students Youssef Hanna and David Samuelson.

News

Aug 2010: Youssef's submission to ICFEM 2010 accepted.

Mar 2010: Golok ver1.2 is now available for download. This version allows for verifying parameterized systems with multiple parameters.

June 2009: Golok ver1.1 is now available for download.

Mar 2009: Youssef's submission to ESEC/FSE 2009 accepted.

About Golok

Golok is a framework for automatic verification of parameterized systems. Given the atomic actions of the processes of the system presented as behavioral automata, the topology of the system and the initial state of the system, Golok automatically generates system-specific cut-off. Golok generates GraphViz source for visualization of the generated cut-off.

Motivation

Parameterized systems are systems consisting of homogeneous processes, where the parameter indicates the number of such processes in the system. A parameterized system, therefore, describes an infinite family of systems where instances of the family can be obtained by fixing the parameter. Verification of correctness of such systems amounts to verifying the correctness of every member of the infinite family described by the system. This problem is undecidable in general.

A number of sound but incomplete verification techniques has been proposed and developed in the recent past. In essence, these techniques depend on computing the invariant or the common global behavior of sys(n) for all n and identifying the smallest k < n such that sys(k) exhibits that behavior. Then it can be shown that a property is satisfied on any system instance sys(n) for any n > k if and only if it is satisfied on sys(k). The problem with current techniques is that they are either manual, cover only certain classes of systems and/or are dependent on the property to be verified.

Golok aims to solve this problem. Golok is a framework for automating cut-off generation of parameterized systems.

Key Features of Golok

  • an interface that allows a user to specify behavioral automata,
  • full automation of cut-off technique including model generation and simulation checking without user intervention
  • a visualization of part of the sys(k) instance that simulates the maximal behavior of a process as a proof of the cut-off value.