模型检测（检验）的流程

使用模型检测技术来进行系统设计的验证包含三个步骤：

建模：第一步需要将设计转化为能被模型检测器接受的形式。在许多情况下这只是简单的编译过程，但在这些时候，由于验证时间和计算机内存的限制，可能还需要使用抽象技术约简不相关或不重要的细节来得到设计的形式化模型。

规约：在验证前，需要声明设计必须满足的性质。性质规约通常是以某种逻辑的形式表示。对硬件与软件系统验证而言，通常使用时序逻辑规约系统的性质，这种逻辑体系能表示系统行为随时间的变化。性质规约过程中最重要的问题是完备性。虽然模型检测提供了检测模型是否满足给定性质的一套方法，但是这套方法并不能保证性质规约确切地表达了待验证系统所需要满足的所有性质。

验证：理想中验证过程应该是完全自动的。但是实际上它常常需要人的协助，其中之一就是分析验证结果。当得到失败的结果后，通常可以给用户提供一个错误轨迹，可以把它看成所有检测性质的一个反例，从而使设计者能够跟踪错误发生的具体位置。当分析错误轨迹并改正系统设计后，需求再次进行模型检测，重新验证，直到验证通过。

错误轨迹也可能由模型建模或刻画性质规约过程的失误导致（常常称为假否定），错误轨迹也能用于确定和修复两类错误。另外，由于计算机的内存限制，当验证过程需要大量内存时，验证可能不会在有限实际内正常终止而产生错误轨迹。这种情况下，需要改变模型检测器的若干参数或直接约简模型，然后重新做验证。

标签：轨迹,错误,验证,规约,检测,流程,检验,模型,性质
来源： https://www.cnblogs.com/longkui-site/p/15859511.html