对时序安全属性检测的一个广泛使用而有效的方法是模型检测(Model Checking)。
模型检测最早由Carnegie Mellon大学的Clark等人提出，其最初用于程序设计、规格说明、协议等较高抽象层次对象和硬件等的正确性检测。随着模型检测技术的不断发展，越来越多的研究人员将模型检测技术应用于程序代码的安全验证。模型检测将原始设计表示成有限状态机，将要验证的性质用时态逻辑描述。然后，遍历有限状态机以检验性质是否存在。有限状态机模型通常采用Kripke结构，在该结构上路径是无限延伸的。模型检测的优点是：全自动进行而无须人机交互。当断定某性质不满足时，模型检测能提供反例，以便于定位设计错误。凭借时态逻辑强大的描述能力，模型检测能够对各种复杂的时序性质进行验证。 状态空间爆炸问题是模型检测的主要缺点。可以说，模型检测技术的发展历史就是不断寻找新思路、新策略和新算法来克服空间爆炸问题的历史。
将程序建模也存在一些缺点，建模本身要消耗资源有时甚至是很多资源，许多建模需要人工干预，无疑这是项枯燥而需耐心的工作，模型与程序本身不可避免的存在语义鸿沟，不能恰如其分的描述程序，一旦程序发生变更，模型也要相应重建。因此，现在也有很多人力图避免建模的过程，而企图直接针对源码进行检测。
由于状态爆炸问题，检测过程中经常忽略一些信息，比如数据流信息，检测得到的结果就会存在漏报和误报，它们之间是一种此消彼长的关系，综合检测效率如何得到合理的折中也很很多方法考虑的问题。
模型检测的优点：有较强的理论基础，形式化程度高，为证明提供了较好的基础；自动化程度高，一旦准备工作完成，可自动进行检测，对检测人员要求低；建立的漏洞库具有通用性，可以检测所有软件的同类型漏洞；能给出漏洞的反例路径，便于排错并修订程序；检测完整，理论上能穷举所有状态。