Verification of Asynchronous Parameterized Networks

Various model checking generalizations were of concern to researchers for several decades. Among them is the uniform verification problem of parameterized systems, that is to prove that a temporal property is satisfied on every instance of a system consisting of an arbitrary number of homogeneous processes. Although the problem is known to be undecidable in general, a range of techniques for decidable or semi-decidable fragments was proposed to cope with the problem.

We extend the technique of network invariants to check parameterized families generated by a network grammar with respect to the asynchronous parallel composition. The original technique relies on the induction principle and strong simulation preorder in order to reduce the problem to that of checking a specification against a few instances of a family by means of the conventional model checking algorithms. To apply the technique in an asynchronous setting we introduce three simulation relations on labelled transition systems. Semi-block simulation is computed to find invariants whereas block simulation and quasi-block simulation serve to establish the correctness of the extended technique in the proofs.

Based on the proposed extension we implemented the Checker of Asynchronous Parameterized Systems (CheAPS). The tool takes process descriptions in a subset of Promela and a network grammar on input. It generates candidate invariants for non-terminals of the grammar and checks that those models are indeed invariants w.r.t. semi-block simulation. Once invariants for all non-terminals are found, a few models in Promela are generated and passed to Spin, which in turn performs finite-state model checking.

CheAPS has been applied to check parameterised systems of several distributed algorithms and network protocols, namely Chandy-Lamport snapshot algorithm, Awerbuch distributed depth-first search algorithm, and a simplified model of RSVP protocol.