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 true 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 process which is greater (with respect to some preorder relation) than any instance of the parameterized system. At the second stage, as soon as an invariant of the parameterized system is obtained, we verify it by means of conventional model checking tool for temporal logics. To demonstrate the feasibility of quasi-block simulation we implemented this technique and applied it to verification of Resource ReSerVation Protocol (RSVP).
Proceedings of the 1-st International Workshop on Invariant Generation, June 25-26, 2007, Hagenberg, Austria, 2007, Hagenberg, Austria, pp. 41-55.