一种模型检测精确加速的判断方法  

A Method to Determine the Exact Acceleration Efficiency in Model Checking

作　　者：勾利杰 李真[1] 王从银[1,2] 庄雷[1] 

机构地区：[1]郑州大学信息工程学院,郑州450001 [2]吉首大学数学与计算机科学学院,湖南吉首416000

出　　处：《中原工学院学报》2014年第4期37-41,共5页Journal of Zhongyuan University of Technology

基　　金：河南省科技攻关项目(122102210042)

摘　　要：在实时系统中具有不同的时间度量,在用时间自动机进行建模及验证时会引起片段问题,通常的解决办法是向时间自动机添加一个附加环,但是在片段数量较少或片段不满足一定条件时,添加附加环的加速效果并不明显,甚至会降低验证速度。对此,本文提出一种模型检测精确加速的判断方法,通过分析加速过程中的主要参数,推导出了精确加速是否有效的判断条件。实验结果表明,利用这个判定条件可以准确地判断模型是否需要加速。To resolve the fragmentation problem of the symbolic state space due to different time scales in real time systems, exact acceleration techniques has been introduced. By appending an extra cycle to timed automata, exact acceleration addresses the problem without any side-effect to the reachability properties of the timed automata. However, in some cases, extra cycle could not lead to obvious acceleration effect, and even decreases the verification speed. To address this problem, a method to determine the acceleration efficiency is presented. By analyzing the main parameters in acceleration process, a condition to determine whether the exact acceleration is effective is deduced, which makes the exact acceleration technique more effective. Experimental results show that, in most cases, this condition can accurately determine whether a model needs to be accelerated.

关 键 词：模型检测 精确加速 加速效益 加速代价 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]