使用模型检测技术来进行系统设计的验证包含三个步骤：
建模：第一步需要将设计转化为能被模型检测器接受的形式。在许多情况下这只是简单的编译过程，但在这些时候，由于验证时间和计算机内存的限制，可能还需要使用抽象技术约简不相关或不重要的细节来得到设计的形式化模型。
规约：在验证前，需要声明设计必须满足的性质。性质规约通常是以某种逻辑的形式表示。对硬件与软件系统验证而言，通常使用时序逻辑规约系统的性质，这种逻辑体系能表示系统行为随时间的变化。性质规约过程中最重要的问题是完备性。虽然模型检测提供了检测模型是否满足给定性质的一套方法，但是这套方法并不能保证性质规约确切地表达了待验证系统所需要满足的所有性质。
验证：理想中验证过程应该是完全自动的。但是实际上它常常需要人的协助，其中之一就是分析验证结果。当得到失败的结果后，通常可以给用户提供一个错误轨迹，可以把它看成所有检测性质的一个反例，从而使设计者能够跟踪错误发生的具体位置。当分析错误轨迹并改正系统设计后，需求再次进行模型检测，重新验证，直到验证通过。
错误轨迹也可能由模型建模或刻画性质规约过程的失误导致（常常称为假否定），错误轨迹也能用于确定和修复两类错误。另外，由于计算机的内存限制，当验证过程需要大量内存时，验证可能不会在有限实际内正常终止而产生错误轨迹。这种情况下，需要改变模型检测器的若干参数或直接约简模型，然后重新做验证。
标签：轨迹,错误,验证,规约,检测,流程,检验,模型,性质 来源： https://www.cnblogs.com/longkui-site/p/15859511.html
本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享； 2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关； 3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关； 4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除； 5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。