作者：王国卿; 庄雷; 和孟佯; 宋玉; 马岭模型检测时间自动机精确加速可加速环窗口
摘要：时间自动机为实时系统进行建模时,通常会因不同的时间度量而产生大量状态片段,精确加速技术可以有效解决这一类片段问题.精确加速中的关键技术是可加速环窗口的计算,但其计算方法均为人工推演.通过对精确加速计算原理的分析,提出了一种精确加速中可加速环窗口的计算算法,可以选择环中任意入边有环时钟复位的节点作为起始,对识别出的可加速环进行进一步精准压缩.首先,识别出时间自动机中所有可加速环,选取1个未处理的可加速环检测环时钟复位的节点出边是否有环时钟复位;然后,将所记录的节点按照记录顺序连接成1个新环,并重新计算新环各边的边界约束;最后,计算可加速环的窗口.算法根据窗口计算原理,获取影响窗口大小的位置不变式、边界约束、时钟复位等数据,并对无用数据和节点进行约减,压缩了可加速环规模,提高了计算效率.算法为研发精确加速自动检测程序奠定了基础.
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
