Spotlight Abstraction with Shade Clustering - Automatic Verification of Parameterised Systems

Parameterised verification is concerned with checking global properties of systems composed of an arbitrary number of processes. An approach to this undecidable problem is combining symmetry arguments with spotlight abstraction. This allows to construct small models of systems on which the properties can be checked. Spotlight abstraction partitions the systems processes into a spotlight and a shade. Shade processes are summarised into a single approximative component and the 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 property holds 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 under abstraction. Finding suitable clusters is not. straightforward. Moreover, an inadequate clustering can lead to an unnecessary explosion of the abstract state space. Therefore, we present an 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 speed up parameterised verification.