计算机应用研究2016，Vol.33Issue(10)：3036-3040,5.DOI:10.3969/j.issn.1001-3695.2016.10.037
面向复杂随机系统的启发式统计模型检测方法
Heuristic statistical model checking approach for complex stochastic systems
摘要
Abstract
Statistical model checking is an efficient verifying technique.It is suitable for verifying complex stochastic systems, such as distributed algorithm.But its performance drops down when verification is over extremely long path.To address this problem,this paper presented a heuristic statistical model checking approach.In verification stage,it searched for the shortest prefix of path to help pruning.In latter sampling stages,it used these prefixes to determine whether current path satisfied the property.This helped to avoid path verification that was time-consuming.In comparison with PRISM,the results show that it verifies less and samples shorter paths in average.As a result,it can use statistical model checking to verify properties over ex-tremely long paths.关键词
统计模型检测/复杂随机系统/超长路径/最短前缀/启发式算法/PRISMKey words
statistical model checking/complex stochastic system/extremely long path/shortest prefix/heuristic algorithm/PRISM分类
信息技术与安全科学引用本文复制引用
何佳,张敏,郭延楠,吕悦..面向复杂随机系统的启发式统计模型检测方法[J].计算机应用研究,2016,33(10):3036-3040,5.基金项目
国家自然科学基金青年科学基金资助项目（61202105）；国家自然科学基金资助项目 （）
