Formal verification of not fully symmetric systems using counter abstraction

Abstract

Counter abstraction allows us to transform a concurrent system with an unbounded number of agents into a finite-state bounded abstraction, independent of the number of processes present in the implementation. In its general form it is not well suited for verification of parameterised concurrent systems based on message passing that are not fully symmetric and/or use two-way handshaken synchronisation between processes. In this paper we present a method whose main idea is to count processes that are in certain equivalence classes. We use labelled transitions systems to model processes (both implementation and specification) and traces refinement for verification checks. Refinement is checked automatically using the FDR model checker. We illustrate the method on a token ring mutual exclusion algorithm from [P. Wolper and V. Lovinfosse, 1990].