On the verification of asynchronous parameterized networks of communicating processes by model checking.

On the verification of asynchronous parameterized networks of communicating processes by model checking.

I.V. Konnov, V.A. Zakharov.

Abstract

The 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. We consider some aspects of the induction-based technique which assumes the construction of finite invariants of such systems. An invariant process is one which 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 apply it to verification of Dijkstra’s token ring algorithm.

Edition

Proceedings of the Institute for System Programming, vol. 12 (in Russian), 2007, Стр. 37-58.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

For citation

I.V. Konnov, V.A. Zakharov. On the verification of asynchronous parameterized networks of communicating processes by model checking. . Proceedings of the Institute for System Programming, vol. 12 (in Russian), 2007, Стр. 37-58. .

Full text of the paper in pdf (in Russian) Back to the contents of the volume