ISSN 1000-1239 CN 11-1777/TP

计算机研究与发展 ›› 2020, Vol. 57 ›› Issue (1): 214-226.doi: 10.7544/issn1000-1239.2020.20190052

• 软件技术 • 上一篇    下一篇

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

王国卿,庄雷,和孟佯,宋玉,马岭   

  1. (郑州大学信息工程学院 郑州 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   

  1. (School of Information Engineering, Zhengzhou University, Zhengzhou 450001)
  • Online: 2020-01-01
  • Supported 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).

摘要: 时间自动机为实时系统进行建模时,通常会因不同的时间度量而产生大量状态片段,精确加速技术可以有效解决这一类片段问题.精确加速中的关键技术是可加速环窗口的计算,但其计算方法均为人工推演.通过对精确加速计算原理的分析,提出了一种精确加速中可加速环窗口的计算算法,可以选择环中任意入边有环时钟复位的节点作为起始,对识别出的可加速环进行进一步精准压缩.首先,识别出时间自动机中所有可加速环,选取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.

Key words: model checking, timed automata, exact acceleration, acceleratable cycle, window

中图分类号: