Verifying Parameterized Networks

Abstract

This article describes a technique based on network grammars and abstraction to verify families of state-transition systems. The family of state-transition systems is represented by a context-free network grammar. Using the structure of the network grammar our technique constructs a process invariant that simulates all the state-transition systems in the family. A novel idea introduced in this article is the use of regidar languages to express state properties. We have implemented our techniques and verified two nontrivial examples.