首页 | 本学科首页   官方微博 | 高级检索  
     

面向安全攸关系统中小概率事件的统计模型检测
引用本文:杜德慧,程贝,刘静.面向安全攸关系统中小概率事件的统计模型检测[J].软件学报,2015,26(2):305-320.
作者姓名:杜德慧  程贝  刘静
作者单位:上海市高可信重点实验室华东师范大学, 上海 200062,上海市高可信重点实验室华东师范大学, 上海 200062,上海市高可信重点实验室华东师范大学, 上海 200062
基金项目:国家自然科学基金(61472140, 61202104); 上海市自然科学基金(14ZR1412500, 13511503100)
摘    要:在开放运行环境中,安全攸关系统的不确定性行为有可能导致小概率事件的发生,而此类事件的可靠性指标往往很高,小概率事件一旦发生就会产生灾难性的后果,严重威胁到人们的生命、财产安全.因此,评估、预测小概率事件发生的概率,对于提高系统的可靠性具有重要意义.统计模型检测是一种基于模拟的模型验证技术,结合了系统的快速模拟及统计分析技术,能够有效提高模型检测的效率,适用于验证、评估安全攸关系统的可靠性,但其面临的挑战性问题之一是在可接受的样本数量下,使用统计模型检测技术难以预测、评估小概率事件发生的概率.因此,提出一种改进的统计模型检测框架,设计和开发基于机器学习的统计模型检测器,实现在相对较少的样本数量下预测和评估小概率事件发生的概率.结合轨道交通控制系统中避碰控制案例分析,进一步证明改进后的统计模型检测器能够有效预测和评估安全攸关系统中小概率事件发生的概率.

关 键 词:统计模型检测  小概率事件  安全攸关系统  随机混成自动机  机器学习
收稿时间:7/2/2014 12:00:00 AM
修稿时间:2014/10/31 0:00:00

Statistical Model Checking for Rare-Event in Safety-Critical System
DU De-Hui,CHENG Bei and LIU Jing.Statistical Model Checking for Rare-Event in Safety-Critical System[J].Journal of Software,2015,26(2):305-320.
Authors:DU De-Hui  CHENG Bei and LIU Jing
Affiliation:Shanghai Key Laboratory of Trustworthy Computing East China Normal University, Shanghai 200062, China,Shanghai Key Laboratory of Trustworthy Computing East China Normal University, Shanghai 200062, China and Shanghai Key Laboratory of Trustworthy Computing East China Normal University, Shanghai 200062, China
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.
Keywords:statistical model checking  rare-event  safety-critical system  stochastic hybrid automata  machine learning
本文献已被 CNKI 等数据库收录!
点击此处可从《软件学报》浏览原始摘要信息
点击此处可从《软件学报》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号