A Tool for Abstraction in Model Checking

AbstractAbstraction methods have become one of the most interesting topics in the automatic verification of software systems because they can reduce the state space to be explored and allow model checking of more complex systems. Nevertheless, there is a lack of tools actually supporting this technique. One direction for abstracting a system is to transform its formal description (its model) into a simpler version specified in the same language, thus skipping the construction of a specific (model checking) tool for the abstract model. The abstraction of the model should be followed by the abstraction of the temporal formulas to be checked. This paper presents αSpin, a tool for the integration of several abstraction approaches (for models and formulas) into the well known model checker Spin. In particular, αSpin integrates two dual approaches, the classic abstraction method, based on under-approximating properties, and an alternative approach, proposed by the authors, where abstraction provides an over-approximation of the formulas.