University of Minnesota
Software Engineering Center

You are here

Toward Automation for Model Checking Requirement Specifications with Numeric Constraints

Date of Publication: 
September 2002
Associated Research Groups: 
Publication Files: 
Model checking techniques have not been effective in important classes of software systems---systems characterized 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 behaviors 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 techniques. 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.
Requirements Engineering Journal, Vol-7, Issue 4, pp. 225-242 (2002)
@article{CRH:REJounal02, author={Yunja Choi and Sanjai Rayadurgam and Mats P.E. Heimdahl}, title={Toward Automation for Model Checking Requirement Specifications with Numeric Constraints}, journal={Requirements Engineering Journal}, year={2002}, month={December}, volume={7}, number={4}, pages={225--242}, publisher={Springer}, annote = {\commentyunja{ }} }