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 sati...

• Type: Journal
• Year: 2010
• Where: JSC
• Authors: Igor V. Konnov, Vladimir A. Zakharov
• Keywords: Conventional Model, Invariant Generation, JSC 2010, Quasi-block Simulation