（1）外加激励信号要由用户给出, 外加激励信号的时序波形决定了所能查出问题的多少。
　　（2）输出结果乃是外加激励信号作用下该数字系统的反应, 并不表示正确与否。
　　（3）分析输入、输出信号之间的关系, 判断该数字系统是否正确的责任落在用户本人的肩上。
　　（4）因此, 受用户给定的外加激励信号质量的影响及用户判断能力的影响, 很难保证现存错误都能查出。
　
　　形式验证研究于七十年代中期开始, 目前还处在发展阶段。本书第6章将介绍其基本理论和方法。