随机混成系统稀有属性的统计模型检测方法
CSTR:
作者:
作者单位:

作者简介:

系统软件与软件工程

通讯作者:

黄志球,zqhuang@nuaa.edu.cn

中图分类号:

TP311

基金项目:

国家重点研发计划(2016YFB1000802,2018YFB1003902);高安全系统软件开发与验证技术工业和信息化部重点实验室(南京航空航天大学)研究项目(NJ2019006)


Statistical Model Checking for Verification of Rare Properties of Stochastic Hybrid System
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    统计模型检测,已成为随机混成系统安全性验证的重要方法.但对安全性要求较高的系统,其不安全事件和系统失效都是稀有事件.在这种情况下,统计模型检测很难采样到满足稀有属性的样本而变得不可行.针对该问题,提出了交叉熵迭代学习的统计模型检测方法首先,使用连续时间马尔可夫链表示随机混成系统的路径概率空间,推导出路径空间上的参数化概率分布函数族;然后构造了随机混成系统路径空间上的交叉熵优化模型,提出了在路径空间上迭代学习最优重要性采样分布的算法;最后给出了基于重要性采样的稀有属性验证算法.实验结果表明:该方法能够有效地对随机混成系统的稀有属性进行验证;且在相同样本数量下,与一些启发式重要性采样方法相比,该方法的估计值能够更好地分布在均值附近,标准方差和相对误差减少超过了一个数量级.

    Abstract:

    Statistical model checking (SMC) is an important method for the verification of safety of stochastic hybrid system (SHS), while for the system with extremely high safety requirements, the unsafe events and the failures of the system are rare events. In this case, it is difficult for SMC to draw the samples satisfying the rare properties and the SMC becomes infeasible. To solve this problem, an SMC method based on cross entropy iterative learning is proposed in this study. First, a continuous time Markov chain (CTMC) is used to represent the path probability space of the SHS, and based on the path space, a parameterized probability distribution family is derived. Then, the cross-entropy optimization model on the path space is constructed and an iterative learning algorithm is proposed, which can find the optimal importance distribution in the path space. Finally, an algorithm for verification of rare properties is given. Experimental results show that the proposed method can effectively verify rare properties of the SHS, and compared with some heuristic importance sampling methods, in the same number of samples, the estimated value of the proposed method can be better distributed near the sample mean, and the standard deviation and relative error are reduced by more than an order of magnitude.

    参考文献
    相似文献
    引证文献
引用本文

房丙午,黄志球,谢健.随机混成系统稀有属性的统计模型检测方法.软件学报,2022,33(10):3717-3731

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2020-03-02
  • 最后修改日期:2020-12-04
  • 录用日期:
  • 在线发布日期: 2022-10-13
  • 出版日期: 2022-10-06
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号