Toward automated verification of software specifications with numeric constraints
Mats P. E. Heimdahl, Yunja Choi · 2003
Model checking is a promising technique for automated verification and validation in the early stage of safety critical software development. Nevertheless, the routine use of the technique in practice has not been possible mainly because of the lack of tool support that integrates the technique into the engineering process and the limitation of the technique to relatively small scale finite state systems. In particular, model checking techniques have not been effective in important classes of software systems—systems characterized by large (or infinite) input domains with interrelated constraints over the system variables. Various process is manual and requires a great deal of ingenuity, or (2) the require special purpose model checkers. data values that subsume all possible system behaviors. The technique is more generally applicable than previously proposed techniques in the sense that it is independent of specific model checking techniques, and thus, can naturally blend into the verification process regardless of which tools are being used. Applications of a prototype implementation of the technique show its promise in practice.