Ivannikov Institute for System Programming of the RAS


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

Authors

Konnov I.V., Zakharov V.A.

Abstract

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

Text of article

Keywords

program verification, asynchronous networks, invariant generation, induction, simulation, model checking

Edition

Journal of Symbolic Computation, Academic Press (United States),vol. 45, № 11, pp. 1144-1162.

Research Group

Theoretical Computer Science

All publications during 2010 All publications