Using abstractions for heuristic state space exploration of reactive object-oriented systems

We present a novel framework for symbolically exploring very large or infinite state spaces of concurrent reactive object-oriented systems. In our framework we apply A* directed search algorithms for performing an efficient heuristic state space exploration towards user-defined search goals. The used heuristics exploit semantical knowledge about a system when searching for specific properties. The knowledge is extracted prior to the search process by computing abstractions of the considered systems. Based on an abstraction and a search goal we generate a heuristic function which can be used during state space exploration of the concrete system. The heuristics can be generated fully automatically and with different precision. Our approach to state space exploration has been implemented in a tool set called HORSE. The tool set can work in combination with an industrial UML case tool, and we show the applicability of our approach by applying the tool set to several sample models.