终止性验证(terminatory validation),理学-计算机科学技术-软件工程-软件工程管理,根据可终止性判定规则,检验被验证对象是否达到终止态。终止性验证可从正向和反向两个方向进行。正向验证终止性是从正向的角度寻找证据,证明被验证对象不存在状态无限循环、无法终止的状况;反向验证终止性是从方向的角度,寻找一条无穷循环的路径或者方法,从而证明被验证对象不终止。被验证对象可以是软件、需求,也可以是规约和设计等个体。被验证对象的终止性分为可终止和不可终止。如果被验证对象经过一系列变迁,最终能够达到预期状态,那么该验证对象是可终止的,否则就是不可终止的。终止性验证可采用传统验证方法进行,也可采用形式化验证方法进行。传统验证方法包括测试和模拟,但这种方法受限于测试用例或模拟样本的可穷性,不能覆盖所有情况,所得到的结果在准确性和可靠性上有欠缺。形式化验证方法是从数学上完备地证明被验证对象是否实现了预期功能或者达到预期状态的一种方法,其验证结果是根据严密的数理逻辑推导而出,所以得到的结果具有准确性和完备性。形式化验证方法是对传统验证方法的一种重要补充,且更为客观、科学。