(郑州大学信息工程学院 郑州 450001) (iegqwang@163.com)
出版日期: 2020-01-01基金资助:国家自然科学基金重点项目(U1604262)；河南省高等学校重点科研项目(19A520003,17A520057)；河南省科技攻关计划项目(172102210478)Calculation Principle and Algorithm for the Window of Exact Acceleration in Real-Time Model Checking
Wang Guoqing, Zhuang Lei, He Mengyang, Song Yu, Ma Ling(School of Information Engineering, Zhengzhou University, Zhengzhou 450001)
Online: 2020-01-01Supported by:This work was supported by the Key Program of the National Natural Science Foundation of China (U1604262), the Key Scientific Research Project of Higher Education of Henan (19A520003, 17A520057), and the Science and Technology Key Project of Henan (172102210478).摘要/Abstract
摘要： 时间自动机为实时系统进行建模时，通常会因不同的时间度量而产生大量状态片段，精确加速技术可以有效解决这一类片段问题.精确加速中的关键技术是可加速环窗口的计算，但其计算方法均为人工推演.通过对精确加速计算原理的分析，提出了一种精确加速中可加速环窗口的计算算法，可以选择环中任意入边有环时钟复位的节点作为起始，对识别出的可加速环进行进一步精准压缩.首先，识别出时间自动机中所有可加速环，选取1个未处理的可加速环检测环时钟复位的节点出边是否有环时钟复位；然后，将所记录的节点按照记录顺序连接成1个新环，并重新计算新环各边的边界约束；最后，计算可加速环的窗口.算法根据窗口计算原理，获取影响窗口大小的位置不变式、边界约束、时钟复位等数据，并对无用数据和节点进行约减，压缩了可加速环规模，提高了计算效率.算法为研发精确加速自动检测程序奠定了基础.
参考文献
相关文章 15
| [1] | 曹彦，黄志球，阚双龙，彭焕峰，柯昌博. 位置约束的访问控制模型及验证方法[J]. 计算机研究与发展, 2018, 55(8): 1809-1825. |
| [2] | 王玲,孟建瑶. 基于特征变权的动态模糊特征选择算法[J]. 计算机研究与发展, 2018, 55(5): 893-907. |
| [3] | 张珩, 张立波, 武延军. 基于Multi-GPU平台的大规模图数据处理[J]. 计算机研究与发展, 2018, 55(2): 273-288. |
| [4] | 季一木,张永潘,郎贤波,张殿超,王汝传. 面向流数据的决策树分类算法并行化[J]. 计算机研究与发展, 2017, 54(9): 1945-1957. |
| [5] | 闻英友,王少鹏,赵宏. 界标窗口下数据流最大规范模式挖掘算法研究[J]. 计算机研究与发展, 2017, 54(1): 94-110. |
| [6] | 段钊,田聪,段振华. 基于CEGAR的C程序空指针解引用检测[J]. 计算机研究与发展, 2016, 53(1): 155-164. |
| [7] | 魏欧,石玉峰,徐丙凤,黄志球,陈哲. 软件模型检测中的抽象模型研究综述[J]. 计算机研究与发展, 2015, 52(7): 1580-1603. |
| [8] | 张琛,段振华, 田聪,鱼滨. 分布式软件系统交互行为建模、验证与测试[J]. 计算机研究与发展, 2015, 52(7): 1604-1619. |
| [9] | 李文明,叶笑春,王达,郑方,李宏亮,林晗,范东睿,孙凝晖. MACT：高通量众核处理器离散访存请求批量处理机制[J]. 计算机研究与发展, 2015, 52(6): 1254-1265. |
| [10] | 符宁,杜承烈,李建良,刘志强,彭寒. AADL分级调度模型的分析与验证[J]. 计算机研究与发展, 2015, 52(1): 167-176. |
| [11] | 刘义海,张效民,沈殷隽,于 洋. 基于窗口统计量的水下分布式目标检测算法[J]. 计算机研究与发展, 2014, 51(8): 1880-1887. |
| [12] | 逄涛,段振华. WISHBONE片上总线符号模型检测[J]. 计算机研究与发展, 2014, 51(12): 2759-2771. |
| [13] | 郑黎明, 邹 鹏, 韩伟红, 李爱平, 贾 焰,. 基于多维熵值分类的骨干网流量异常检测研究[J]. , 2012, 49(9): 1972-1981. |
| [14] | 王 爽, 王国仁,. 基于滑动窗口的Top-K概率频繁项查询算法研究[J]. , 2012, 49(10): 2189-2197. |
| [15] | 王 雷 陈 归 金茂忠. 基于约束分析与模型检测的代码安全漏洞检测方法研究[J]. , 2011, 48(9): 1659-1666. |
PDF全文下载地址:
https://crad.ict.ac.cn/CN/article/downloadArticleFile.do?attachType=PDF&id=4090
