王国卿, 庄雷, 和孟佯, 宋玉, 马岭. 实时模型检测精确加速窗口的计算原理及算法[J]. 计算机研究与发展, 2020, 57(1): 214-226.
 引用本文: 王国卿, 庄雷, 和孟佯, 宋玉, 马岭. 实时模型检测精确加速窗口的计算原理及算法[J]. 计算机研究与发展, 2020, 57(1): 214-226.
Wang Guoqing, Zhuang Lei, He Mengyang, Song Yu, Ma Ling. Calculation Principle and Algorithm for the Window of Exact Acceleration in Real-Time Model Checking[J]. Journal of Computer Research and Development, 2020, 57(1): 214-226.
 Citation: Wang Guoqing, Zhuang Lei, He Mengyang, Song Yu, Ma Ling. Calculation Principle and Algorithm for the Window of Exact Acceleration in Real-Time Model Checking[J]. Journal of Computer Research and Development, 2020, 57(1): 214-226.

## Calculation Principle and Algorithm for the Window of Exact Acceleration in Real-Time Model Checking

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

Abstract: When real-time systems are modeled as timed automata, different time scales may lead to a lot of fragmentations of the symbolic state space. This problem can be solved by computing the zones which in practice use the abstraction technique. The state-of-the-art abstraction methods produce an approximation that is closer to the actual reachable clock valuation, which are coarser abstractions. The exact acceleration is a finer abstraction way to reduce the required storage space and it can solve or alleviate the state space explosion problem of the fragmentations. Calculating the acceleratable cycle’s window is the key technology in exact acceleration. The calculation of the window in acceleratable cycle depends on the location invariant, edge constraint and clock reset. By comprehensively analyzing the exact acceleration principle, an algorithm is proposed to calculate the window in exact acceleration. Firstly, it is important to identify all acceleratable cycles in time automaton. Choose one node with clock reset on incoming edge as the start and check whether there is a clock reset on outgoing edge for every nodes. Secondly, all the recorded nodes link as a new cycle according to the recording ordering. Each node in new cycle has the original location invariant and each edge contains clock reset. In addition, edge constraints need to calculate. Finally, the window of acceleratable cycle can denote an interval ［a,b］, where a means the sum of edge constraints and b means the sum of location invariants. The time complexity of the algorithm is O(n\+2). According to the calculation principle, the algorithm can get the valid data of the window, reduce other useless data and nodes, compress the acceleratable cycle, make the model simpler and enhance the computing efficiency. The algorithm lays the foundation for the research and development of the automatic model checking program.

/

• 分享
• 用微信扫码二维码

分享至好友和朋友圈