模型检测（model detection），理学-计算机科学技术-信息安全-信息系统安全-软件安全-软件安全防御，一种有限状态系统的自动验证技术。可以彻底地、自动地检查给定硬件或软件系统的模型是否符合给定的属性和规范。模型检测的基本思想是用状态迁移系统（S）表示系统的行为，用模态逻辑公式（F）描述系统的性质。这样“系统是否具有所期望的性质”就转化为数学问题“状态迁移系统S是否是公式F的一个模型?”，用公式表示为S╞F。对有穷状态系统，这个问题是可判定的，即可以用计算机程序在有限时间内自动确定。从模型表达方式上，模型检测分为显式状态模型检测和符号模型检测两种。显式状态模型检测使用有穷状态自动机来表示，而符号模型检测常用逻辑公式、二叉决策图（BDD）或其他数据结构来表示。被验证的属性常常使用线性时序逻辑（LTL）、正则公式、计算树逻辑（CTL）来表示。模型检测是一种重要的自动验证技术，并能在系统不满足性质时提供反例路径，因此在工业界比正确性证明更受推崇。模型检测可以应用于如硬件控制器和通信协议这些有穷状态系统。同时，也可以同各种抽象和归纳原则结合起来验证非有穷状态系统（如实时系统）。