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

Clc Number:

TP311

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:March 02,2020
  • Revised:December 04,2020
  • Adopted:
  • Online: October 13,2022
  • Published: October 06,2022
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063