面向安全攸关系统中小概率事件的统计模型检测
作者:
基金项目:

国家自然科学基金(61472140, 61202104); 上海市自然科学基金(14ZR1412500, 13511503100)


Statistical Model Checking for Rare-Event in Safety-Critical System
Author:
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [31]
  • |
  • 相似文献 [20]
  • |
  • 引证文献
  • | |
  • 文章评论
    摘要:

    在开放运行环境中,安全攸关系统的不确定性行为有可能导致小概率事件的发生,而此类事件的可靠性指标往往很高,小概率事件一旦发生就会产生灾难性的后果,严重威胁到人们的生命、财产安全.因此,评估、预测小概率事件发生的概率,对于提高系统的可靠性具有重要意义.统计模型检测是一种基于模拟的模型验证技术,结合了系统的快速模拟及统计分析技术,能够有效提高模型检测的效率,适用于验证、评估安全攸关系统的可靠性,但其面临的挑战性问题之一是在可接受的样本数量下,使用统计模型检测技术难以预测、评估小概率事件发生的概率.因此,提出一种改进的统计模型检测框架,设计和开发基于机器学习的统计模型检测器,实现在相对较少的样本数量下预测和评估小概率事件发生的概率.结合轨道交通控制系统中避碰控制案例分析,进一步证明改进后的统计模型检测器能够有效预测和评估安全攸关系统中小概率事件发生的概率.

    Abstract:

    In open environment, the stochastic behavior of safety-critical system may lead to occurrence of rare-event, which is critical to the system's reliability. It is very important to estimate the probability of rare-event occurrence. Statistical model checking (SMC) is a simulation-based model checking technology, which integrates the simulation and statistical analysis technique to improve the efficiency of traditional model checking. SMC is used to verify and estimate the reliability of complex safety-critical system. However, the most challenging problem is that it is impossible to estimate and predict the probability of rare-event based on SMC with the acceptable sample size. To solve this problem, this study proposes an improved statistical model checking framework, designs and develops a statistical model checker based on machine learning to estimate and predict the probability of rare-event with fewer sample size. To demonstrate the presented approach, a case study on collision avoidance system in CBTC is discussed. The analysis results show that the proposed approach is feasible and efficient.

    参考文献
    [1] Mitra S, Wongpiromsarn T, Murray RM. Verifying cyber-physical interactions in safety-critical systems. Security & Privacy, 2013, 11(4):28-37.[doi: 10.1109/MSP.2013.77]
    [2] Michael L, Frank O. Teaching and training formal methods for safety critical systems. In: Proc. of the 39th Euromicro Conf. on Software Engineering and Advanced Applications (SEAA). IEEE, 2013. 408-413.[doi: 10.1109/SEAA.2013.54]
    [3] Zuliani P, Baier C, Clarke EM. Rare-Event verification for stochastic hybrid systems. In: Proc. of the 15th ACM Int'l Conf. on Hybrid Systems: Computation and Control. ACM Press, 2012. 217-226.[doi: 10.1145/2185632.2185665]
    [4] Clarke EM, Klieber W, Nováček M, Zuliani P. Model checking and the state explosion problem. In: Meyer B, Nordio M, eds. Proc. of the LASER 2012. LNCS 7682, Heidelberg: Springer-Verlag, 2012. 1-30.[doi: 10.1007/978-3-642-35746-6_1]
    [5] Clarke EM, Zuliani P. Statistical model checking for cyber-physical systems In: Proc. of the Automated Technology for Verification and Analysis. Heidelberg: Springer-Verlag, 2011. 1-12.[doi: 10.1007/978-3-642-24372-1_1]
    [6] David A, Larsen KG, Legay A, Mikučionis M. Schedulability of herschel-planck revisited using statistical model checking. In: Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies. Berlin, Heidelberg: Springer-Verlag, 2012. 293-307.[doi: 10.1007/978-3-642-34032-1_28]
    [7] Jha SK, Clarke EM, Langmead CJ, Legay A, Platzer A, Zuliani P. A bayesian approach to model checking biological systems. In: Proc. of the Computational Methods in Systems Biology. Heidelberg: Springer-Verlag, 2009. 218-234.[doi: 10.1007/978-3-642-03845-7_15]
    [8] Miskov-Zivanov N, Zuliani P, Clarke EM, Faeder JR. Studies of biological networks with statistical model checking: application to immune system cells. In: Proc. of the Int'l Conf. on Bioinformatics, Computational Biology and Biomedical Informatics. ACM Press, 2013. 728-729.[doi: 10.1145/2506583.2512390]
    [9] David A, Du DH, Larsen KG, Mikučionis M, Skou A. An evaluation framework for energy aware buildings using statistical model checking. Science China Information Sciences, 2012,55(12):2694-2707.[doi: 10.1007/s11432-012-4742-0]
    [10] Legay A, Delahaye B, Bensalem S. Statistical model checking: An overview. In: Proc. of the Runtime Verification. Heidelberg: Springer-Verlag, 2010. 122-135.[doi: 10.1007/978-3-642-16612-9_11]
    [11] David A, Du D, Larsen KG, Legay A, Mikučionis M, Poulsen DB, Sedwards S. Statistical model checking for stochastic hybrid systems. arXiv preprint arXiv:1208.3856, 2012.[doi: 10.4204/EPTCS.92.9]
    [12] Bulychev P, David A, Larsen KG, Mikučionis M, Poulsen DB, Legay A, Wang Z. UPPAAL-SMC: Statistical model checking for priced timed automata. arXiv preprint arXiv:1207.1272, 2012.[doi: 10.4204/EPTCS.85.1]
    [13] David A, Larsen KG, Legay A, Mikučionis M, Poulsen DB, Van Vliet J, Wang Z. Statistical model checking for networks of priced timed automata. In: Proc. of the Formal Modeling and Analysis of Timed Systems. Heidelberg: Springer-Verlag, 2011. 80-96.[doi: 10.1007/978-3-642-24310-3_7]
    [14] Villén-Altamirano M, Villén-Altamirano J. RESTART: A straightforward method for fast simulation of rare events. In: Proc. of the Simulation Conf. IEEE, 1994. 282-289.[doi: 10.1109/WSC.1994.717150]
    [15] Cortes C, Vapnik V. Support-Vector networks. Machine Learning, 1995,20(3):273-297.[doi: 10.1007/BF00994018]
    [16] Press WH. Numerical Recipes 3rd ed., The Art of Scientific Computing. Cambridge: Cambridge University Press, 2007.
    [17] Li R, Ye SW, Shi ZZ. SVM-KNN classifier—A new method of improving the accuracy of SVM classifier. Acta Electronica Sinica, 2002,30(5):745-748 (in Chinese with English abstract).[doi: 10.3321/j.issn:0372-2112.2002.05.035]
    [18] Ling P, Zhou CG. For SVM: Confidence online evaluation & decision improvement. Journal of Frontiers of Computer Science & Technology, 2008,2(2):192-197 (in Chinese with English abstract).[doi: 10.3778/j.issn.1673-9418.2008.02.007]
    [19] Diehl CP, Cauwenberghs G. SVM incremental learning, adaptation and optimization. Proc. of the Int'l Joint Conf. on IEEE, 2003,4: 2685-2690.[doi: 10.1109/IJCNN.2003.1223991]
    [20] Qian HB, He GN. A survey of class-imbalanced data classification. Computer Engineering and Science, 2010,32(5):85-88 (in Chinese with English abstract).[doi: 10.3969/j.issn.1007-130X.2010.05.023]
    [21] Chang CC, Lin CJ. LIBSVM: A library for support vector machines. ACM Trans. on Intelligent Systems and Technology, 2011,2 (3):1-27.[doi: 10.1145/1961189.1961199]
    [22] Kim Y, Kim M, Kim TH. Statistical model checking for safety critical hybrid systems: An empirical evaluation. In: Armin B, Amir N, Tanja V, eds. Proc. of the Hardware and Software: Verification and Testing. Heidelberg: Springer-Verlag, 2013. 162-177.[doi: 10.1007/978-3-642-39611-3_18]
    [23] Zuliani P, Platzer A, Clarke EM. Bayesian statistical model checking with application to Stateflow/Simulink verification. Formal Methods in System Design, 2013,43(2):338-367.[doi: 10.1007/s10703-013-0195-3]
    [24] Zhu L, Yu FR, Ning B, Tang, T. Communication-Based train control (CBTC) systems with cooperative relaying: Design and performance analysis. IEEE Trans. on Vehicular Technology, 2013,63(5):2162-2172.[doi: 10.1109/TVT.2013.2291533]
    [25] Damm W, Mikschl A, Oehlerking J, Olderog ER, Pang J, Platzer A, Wirtz B. Automating verification of cooperation, control, and design in traffic applications. In: Proc. of the Formal Methods and Hybrid Real-Time Systems. Heidelberg: Springer-Verlag, 2007. 115-169.[doi: 10.1007/978-3-540-75221-9_6]
    [26] Zhang YP, Sun YS, Zhao B. Research on train interval control under moving block. Highlights of Sciencepaper Online, 2013,6(12): 1112-1118 (in Chinese with English abstract).
    [27] Srinivasan R. Importance Sampling: Applications in Communications and Detection. Heidelberg: Springer-Verlag, 2002.
    [28] Jegourel C, Legay A, Sedwards S. Cross-Entropy optimisation of importance sampling parameters for statistical model checking. In: Proc. of the Computer Aided Verification. Heidelberg: Springer-Verlag, 2012. 327-342.[doi: 10.1007/978-3-642-31424-7_26]
    [29] Gong H, Wu TT, Clarke EM. Pathway-Gene identification for pancreatic cancer survival via doubly regularized Cox regression. BMC Systems Biology, 2014,8(1):1-9.[doi: 10.1186/1752-0509-8-S1-S3]
    [30] Zhang DP, Nie CH, Xu BW. Importance sampling method of software reliability estimation. Ruan Jian Xue Bao/Journal of Software, 2009,20(10):2859-2866 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/3553.htm[doi: 10.3724/SP. J.1001.2009.03553]
    [31] Zimmermann A, Trowitzsch J. Reliability evaluation of distributed embedded systems with UML state charts and rare event simulation. In: Proc. of the MBEES. 2009. 128-139.
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

杜德慧,程贝,刘静.面向安全攸关系统中小概率事件的统计模型检测.软件学报,2015,26(2):305-320

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

京公网安备 11040202500063号