CSP-based counter abstraction for systems with node identifiers

• We consider the Parameterised Model Checking Problem for CSP.
• Systems are built from similar node processes, which may use one another’s identities, embedded in a context.
• We build abstract models for this situation, using the technique of counter abstraction.
• We show these models form abstractions of the considered systems, in both the traces and stable failures models.
• We show how this can be used to deduce correctness of the considered systems.

The Parameterised Model Checking Problem asks whether an implementation Impl(t) satisfies a specification Spec(t) for all instantiations of parameter  t. In general, t  can determine numerous entities: the number of processes used in a network, the type of data, the capacities of buffers, etc. The main theme of this paper is automation of uniform verification of a subclass of PMCP with the parameter of the first kind, i.e. where it determines the number of processes used in a network. We use CSP as our formalism.Counter abstraction is a technique that replaces a concrete state space by an abstract one, where each abstract state is a tuple of integer counters (c1,…,ck) such that for each  i, ci counts how many node processes are currently in the i-th state. Each counter ci is given a finite threshold zi and we interpret ci=zi as there being zi or more processes in the i-th state.Standard counter abstraction techniques require all processes to be identical, which means that nodes cannot use node identifiers. In this paper we present how counter abstraction techniques can be extended to processes that make use of node identifiers in a symmetrical way. Our method creates a process Abstr that is independent of  t and is refined by ϕ(Impl(T)) for all sufficiently large  T, where ϕ maps all (sufficiently large) instantiations T of the parameter to some fixed type. By transitivity of refinement, testing if Abstr refines Spec(ϕ(t)) implies that Spec(ϕ(t)) is refined by ϕ(Impl(T)). Then, using the type reduction theory from Mazur and Lowe (2012) [29], we can deduce that Spec(T) is refined by Impl(T) for all sufficiently large T, thus obtaining a positive answer to the original verification problem.