Journal of Software:2015.26(2):305-320

(上海市高可信重点实验室华东师范大学, 上海 200062)
Statistical Model Checking for Rare-Event in Safety-Critical System
DU De-Hui,CHENG Bei,LIU Jing
(Shanghai Key Laboratory of Trustworthy Computing East China Normal University, Shanghai 200062, China)
Chart / table
Similar Articles
Article :Browse 4226   Download 3369
Received:July 02, 2014    Revised:October 31, 2014
> 中文摘要: 在开放运行环境中,安全攸关系统的不确定性行为有可能导致小概率事件的发生,而此类事件的可靠性指标往往很高,小概率事件一旦发生就会产生灾难性的后果,严重威胁到人们的生命、财产安全.因此,评估、预测小概率事件发生的概率,对于提高系统的可靠性具有重要意义.统计模型检测是一种基于模拟的模型验证技术,结合了系统的快速模拟及统计分析技术,能够有效提高模型检测的效率,适用于验证、评估安全攸关系统的可靠性,但其面临的挑战性问题之一是在可接受的样本数量下,使用统计模型检测技术难以预测、评估小概率事件发生的概率.因此,提出一种改进的统计模型检测框架,设计和开发基于机器学习的统计模型检测器,实现在相对较少的样本数量下预测和评估小概率事件发生的概率.结合轨道交通控制系统中避碰控制案例分析,进一步证明改进后的统计模型检测器能够有效预测和评估安全攸关系统中小概率事件发生的概率.
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.
文章编号:     中图分类号:    文献标志码:
基金项目:国家自然科学基金(61472140, 61202104); 上海市自然科学基金(14ZR1412500, 13511503100) 国家自然科学基金(61472140, 61202104); 上海市自然科学基金(14ZR1412500, 13511503100)
Foundation items:
Reference text:


DU De-Hui,CHENG Bei,LIU Jing.Statistical Model Checking for Rare-Event in Safety-Critical System.Journal of Software,2015,26(2):305-320