Sciweavers

Share
JSC
2010

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

9 years 9 months ago
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...
Igor V. Konnov, Vladimir A. Zakharov
Added 19 May 2011
Updated 19 May 2011
Type Journal
Year 2010
Where JSC
Authors Igor V. Konnov, Vladimir A. Zakharov
Comments (0)
books