Spotlight Abstraction with Shade Clustering -- Automatic Verification of Parameterised Systems

Parameterised verification is concerned with checking global properties of software systems composed of an arbitrary number of processes. A promising approach to this generally undecidable problem is combining symmetry arguments with spotlight abstraction. This combination allows to construct small abstract models of parameterised systems on which the properties can be checked. Spotlight abstraction partitions the systems processes into a spotlight and a shade. The processes in the shade are summarised into a single approximative component and the inherent loss of information is modelled by a third truth value unknown. Thus, a verification run may also return unknown, which does not allow to draw any conclusions whether the system satisfies the property or not. Here we introduce an extension of spotlight abstraction called shade clustering, which allows to divide the shade into multiple approximative components, and thus, to preserve more definite information in the abstract model. Finding suitable clusters is, however, not straightforward. Moreover, an inadequate clustering can easily lead to an unnecessary explosion of the abstract state space. Therefore, we also present a fully automatic abstraction refinement framework for verifying parameterised systems. Based on abstract counterexamples, refinement is iteratively performed by either adding new predicates, shifting processes from the shade to the spotlight, or building appropriate shade clusters. Experimental results show that our shade clustering-based approach can significantly reduce the number of necessary refinement steps and thus speed up parameterised verification.