目前软件工程中的验证与测试技术正不断融合,相互借鉴,共同为提高软件的安全性、可靠性做出努力。验证的模型检测方法可以应用于测试当中,而经过测试所得出的一致性结论又可以对验证进行补充和完善。所以在当今的软件证实方法中,验证和测试起着相互补充的作用。而从长远发展来看,验证技术和测试技术也必将结合的更加紧密。论文以ioco一致性关系所存在的安全性缺陷为切入点,利用对软件进行模型检测的方法,成功的解决了由于测试的局限性所带来的具体的系统安全性问题。为了完成这项工作,本文主要做了以下几个方面的工作：(1)研究了ioco一致性的两类安全性缺陷,并由此引申出了违背系统安全性的定义；(2)提出了寻找系统安全性问题的SDR算法,并利用现有的程序模型检测工具找到系统中存在的安全性问题；(3)对所找到的违背系统安全性的迹,根据其不同的类型实施不同的处理,使得系统的安全性问题最终得到彻底的解决。在实验阶段,本文使用咖啡机的例子说明了该软件工程方法的实际流转程序,并使用上述的软件工程方法对ATM系统进行了分析并找到了违背安全性的反例。