Towards scaling up DynAlloy analysis using predicate abstraction

Abstract

DynAlloy is an extension to the Alloy specifi cation language suitable for modeling properties of executions of software systems. DynAlloy provides fully automated support for verifying properties of programs, in the style of the Alloy Analyzer, i.e., by exhaustively searching for counterexamples of properties in bounded scenarios (bounded domains and iterations of programs). But, as for other automated analysis techniques, the so called state explotion problem makes the analysis feasible only for small bounds. In this paper, we take advantage of an abstraction technique known as predicate abstraction, for scaling up the analysis of DynAlloy specifi cations. The implementation of predicate abstraction we present enables us to substantially increase the domain and iteration bounds in some case studies, and its use is fully automated. Our implementation is relatively e cient, exploiting the reuse of already calculated abstractions when these are available, and an "on the fly" check of traces when looking for counterexamples. We introduce the implementation of the technique, and some preliminary experimental results with case studies, to illustrate the benefi ts of the technique.