面向安全攸关系统中小概率事件的统计模型检测  

Statistical Model Checking for Rare-Event in Safety-Critical System

作　　者：杜德慧[1] 程贝[1] 刘静[1] 

机构地区：[1]上海市高可信重点实验室(华东师范大学),上海200062

出　　处：《软件学报》2015年第2期305-320,共16页Journal of Software

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

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

关 键 词：统计模型检测 小概率事件 安全攸关系统 随机混成自动机 机器学习 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]