首页 期刊 计算机研究与发展 实时模型检测精确加速窗口的计算原理及算法 【正文】

实时模型检测精确加速窗口的计算原理及算法

作者:王国卿; 庄雷; 和孟佯; 宋玉; 马岭 郑州大学信息工程学院; 郑州450001
模型检测   时间自动机   精确加速   可加速环   窗口  

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

注:因版权方要求,不能公开全文,如需全文,请咨询杂志社

学术咨询 免费咨询 杂志订阅