An invariant-based approach to the verification of asynchronous parameterized networks

摘要

A uniform verification problem for parameterized systems is to determine whether a temporal property is satisfied for every instance of the system which is composed of an arbitrary number of homogeneous processes. To cope with this problem we combine an induction-based technique for invariant generation and conventional model checking of finite state systems. At the first stage of verification we try to select automatically an appropriate invariant system. At the second stage, as soon as an invariant of the parameterized system is obtained, we verify it by means of a conventional model checking tool for temporal logics. An invariant system is one that is greater (with respect to some preorder relation) than any instance of the parameterized system. Therefore, the preorder relation involved in the invariant rule is of considerable importance. For this purpose we introduce a new type of simulation preorder -quasi-block simulation. We show that quasi-block simulation preserves the satisfiability of formulae from ACTL~*-X and that asynchronous composition of processes is monotonic w.r.t. quasi-block simulation. This suggests the use of quasi-block simulation in the induction-based verification techniques for asynchronous networks. To demonstrate the feasibility of quasi-block simulation we implemented this technique and applied it to the verification of the Resource Reservation Protocol (RSVP).