Toward Automation for Model-Checking Requirements Specifications with Numeric Constraints

Model-checking techniques have not been effective in important classes of software systems – systems characterised by large (or infinite) input domains with interrelated linear and non-linear constraints over the system variables. Various model abstraction techniques have been proposed to address this problem, but their effectiveness in practice is limited by two factors: first, the abstraction process is manual and requires a great deal of ingenuity; and, second, the abstraction may be coarse and introduce too many spurious behaviours to provide meaningful analysis results. In this paper, we wish to propose domain reduction abstraction based on data equivalence and trajectory reduction as an alternative and complement to other abstraction tech niques. Our technique applies the abstraction to the input domain (environment) instead of the model and is applicable to constraint free and deterministic constrained data transition systems. Our technique is automatable with some minor restrictions. We provide formal proofs for the theoretical soundness of the technique, algorithms for automation, and an illustration of the approach with examples. Correspondence and offprint requests to: Mats P. E. Heimdahl, Department of Computer Science and Engineering, University of Minnesota, 200 Union Street SE, 4-192 Minneapolis, MN 55455, USA. E-mail: heimdahl@cs.umn.edu