随机混成系统稀有属性的统计模型检测方法

统计模型检测,已成为随机混成系统安全性验证的重要方法.但对安全性要求较高的系统,其不安全事件和系统失效都是稀有事件.在这种情况下,统计模型检测很难采样到满足稀有属性的样本而变得不可行.针对该问题,提出了交叉熵迭代学习的统计模型检测方法首先,使用连续时间马尔可夫链表示随机混成系统的路径概率空间,推导出路径空间上的参数化概率分布函数族;然后构造了随机混成系统路径空间上的交叉熵优化模型,提出了在路径空间上迭代学习最优重要性采样分布的算法;最后给出了基于重要性采样的稀有属性验证算法.实验结果表明:该方法能够有效地对随机混成系统的稀有属性进行验证;且在相同样本数量下,与一些启发式重要性采样方法相比,该方法的估计值能够更好地分布在均值附近,标准方差和相对误差减少超过了一个数量级.     

基于遗传算法和LSSVM的网络安全事件发生频率预测

网络安全事件发生频率是非线性变化的,传统时序预测方法难以处理;样本数量少时,人工神经网络等方法预测精度也难以保证。最小二乘支持向量机（LSSVM）是一种基于统计学习理论的机器学习方法,能非常好地解决小样本、非线性问题。本文将LSSVM应用于网络安全事件发生频率的预测,为了达到最佳预测效果,使用一种改进的遗传算法对模型参数进行优化。通过实验验证,改进的遗传算法较简单遗传算法收敛更快,优化效率更高,优化后的模型能够达到良好的预测效果。     

一种面向CPS的自适应统计模型检测方法

随着计算机与物理环境的交互日益密切,信息物理融合系统（cyber physical systems,CPSs）在健康医疗、航空电子、智能建筑等领域有着广泛的应用前景,CPSs的正确性、可靠性分析已引起人们的广泛关注.统计模型检测（statistical model checking,SMC）技术能够对CPSs进行有效验证,并为系统的性能提供定量评估.然而,随着系统规模的日益扩大,如何提高统计模型检测技术验证CPSs的效率,是目前所面临的主要困难之一.针对此问题,本文首先对现有SMC技术进行实验分析,总结各种SMC技术的受限适用范围和性能缺陷,并针对贝叶斯区间估计算法（Bayesian Interval Estimate,BIE）在实际概率接近0.5时需要大量路径才能完成验证的缺陷,提出一种基于抽象和学习的统计模型检测方法AL-SMC.该方法采用了主成分分析、前缀树约减等技术,对仿真路径进行学习和抽象,以减少样本空间.接着,提出了一个面向CPS的自适应SMC算法框架,可根据不同的概率区间自动选择AL-SMC算法或者BIE算法,有效应对不同情况下的验证问题.最后,结合经典案例进行实验分析,实验结果表明自适应SMC算法框架能够在一定误差范围内有效提高CPSs统计模型检测的效率,为CPSs的分析验证提供了一种有效的途径.     

改进的人工免疫入侵检测模型

针对现有的人工免疫入侵检测系统存在的缺陷,在Hofmeyr的分布式人工免疫系统(ARTIS)基础上,提出了改进的人工免疫入侵检测模型。在改进模型中,用协议分析技术对免疫模块进行协同刺激,以提高记忆检测器和成熟检测器的质量,并降低检测器的规模;通过按协议生成和组织检测器,解决传统人工免疫系统检测效率低下的问题;采用基于权值的r-连续位匹配规则提高抗体和抗原匹配的准确度;同时协同刺激模块也能够在发生风暴型攻击时自动生成动态防火墙过滤规则,以提高在发生大规模攻击情况下的性能。最后,使用MIT Lincoln实验室的DARPA数据集对改进模型和ARTIS模型进行了模拟测试及对比分析,验证了所提模型的可行性和有效性。     

海洋环境武器效能的改进RBF网络评估模型

文中针对海洋环境影响下单武器装备作战效能的评估问题,建立基于RBF神经网络的评估模型。在实际应用中,为了保证评估结果的客观性和准确性,提出一种基于统计原理的改进RBF神经网络模型。该改进模型采用基于样本相似度的聚类算法,以加权欧氏距离为样本相似性度量方法,通过对样本进行聚类处理得到RBF神经网络模型的参数,进而建立评估模型。最后,为了验证提出模型的可行性,利用样本实例对模型进行训练,并利用训练后的模型对某一环境下单一武器作战效能进行评估,实验结果表明了模型的可行性和可靠性。和传统方法相比,该评估模型基于样本数据的统计信息,不需要专家知识,具有较高的客观性。     

拟贝叶斯推断算法在软件可靠性模型中的应用

本文针对工程软件的可靠性评估,提出了一种基于不精确概率的拟贝叶斯软件可靠性统计推断算法,以区间值概率替代传统贝叶斯可靠性模型中精确概率先验,能更准确地表达专家的模糊信息并避免做出与实际不符的假设。在开目PDM某组件中的应用实践表明,该算法能在小样本的测试数据下快速地逼近模型参数的准确值。     

基于故障剖面的安全关键系统可靠性测试与评估

可靠性测试是安全关键系统可靠性评估的重要手段。论文结合在某电信系统的工程实践,介绍一种基于故障剖面的可靠性测试和评估的方法：通过逆向工程从已有的安全关键系统的失效事件中分析提取出故障概率数据,结合故障注入测试对系统的可靠性进行评估。该方法直接从故障入手,不受缺乏缺陷引发故障概率数据问题的困扰,并通过故障模式的双层模型明确测试范围,简化了评估过程。     

动态事件时间数据的多任务Logistic生存预测方法

事件时间数据广泛存在于临床医学研究领域,包含大量复杂的随时间变化的动态风险因子变量。为了对这些动态事件时间数据进行有效分析,克服生存模型参数假设的局限性,提出了一种多任务Logistic生存学习和预测方法。将生存预测转化为一系列不同时间点的多任务二元生存分类问题,利用动态风险因子变量的全部观测值估计累积风险。通过对事件样本和删失样本的全数据学习正则化Logistic回归参数。评估风险因子与事件时间的动态关系,根据生存概率估计事件时间。在多个实际临床数据集上开展的对比实验验证了提出的多任务预测方法对于动态数据不仅具有较强的适用性,而且能够保障预测结果的准确性和可靠性。     

HNPG步态特征数据库管理系统设计与实现

为增强步态识别算法的评估和验证的可靠性,加速步态识别技术的实际应用进程,针对大量非结构化数据管理问题和当前小样本步态数据库的不足,采用面向对象的数据管理模型,基于平台化的总体思想,设计和实现了一个开放式的基础步态数据支撑平台.提出了包括数据规范、数据采集加工处理、数据管理模式、应用开发和设计等方面的系统解决方案.实践表明系统的数据采集规范、样本数量、步态数据清晰度、基础平台和开放性等指标都超过了同类型的数据库,系统具有较强的扩展性、安全性和可靠性,达到了预期目标.     

改进TOPSIS法的装备可靠性评估方法

装备的可靠性是完成遂行任务必备条件,对装备可靠性进行评估可为任务决策提供理论支持;目前关于装备可靠性评估方面的研究大多数都是基于概率统计学的,而概率统计的准确性受限于样本的大小,从而使得基于概率统计学的装备可靠性评估因装备样本的大小而产生不可避免的或大或小误差;为解决这一评估受样本大小制约的问题,引入逼近理想点(TOPSIS)法;同时,针对TOPSIS法受主观因素影响较大的问题,修定了该法评估指标权重及理想解的确定方法,并在评估结果中引入了“合格分数线”的概念,使得评估结果等级划分有了量化依据,从而体现出了客观性和科学性,然后构建了某装备基于该改进TOPSIS法的可靠性评估模型;最后,通过示例分析,利用MATLAB计算验证了本文方法的正确性,评估结果可为装备的使用者或指挥者提供决策依据。     

Bayesian statistical model checking with application to Stateflow/Simulink verification

We address the problem of model checking stochastic systems, i.e., checking whether a stochastic system satisfies a certain temporal property with a probability greater (or smaller) than a fixed threshold. In particular, we present a Statistical Model Checking (SMC) approach based on Bayesian statistics. We show that our approach is feasible for a certain class of hybrid systems with stochastic transitions, a generalization of Simulink/Stateflow models. Standard approaches to stochastic discrete systems require numerical solutions for large optimization problems and quickly become infeasible with larger state spaces. Generalizations of these techniques to hybrid systems with stochastic effects are even more challenging. The SMC approach was pioneered by Younes and Simmons in the discrete and non-Bayesian case. It solves the verification problem by combining randomized sampling of system traces (which is very efficient for Simulink/Stateflow) with hypothesis testing (i.e., testing against a probability threshold) or estimation (i.e., computing with high probability a value close to the true probability). We believe SMC is essential for scaling up to large Stateflow/Simulink models. While the answer to the verification problem is not guaranteed to be correct, we prove that Bayesian SMC can make the probability of giving a wrong answer arbitrarily small. The advantage is that answers can usually be obtained much faster than with standard, exhaustive model checking techniques. We apply our Bayesian SMC approach to a representative example of stochastic discrete-time hybrid system models in Stateflow/Simulink: a fuel control system featuring hybrid behavior and fault tolerance. We show that our technique enables faster verification than state-of-the-art statistical techniques. We emphasize that Bayesian SMC is by no means restricted to Stateflow/Simulink models. It is in principle applicable to a variety of stochastic models from other domains, e.g., systems biology.     

AL-SMC: Optimizing Statistical Model Checking by Automatic Abstraction and Learning

Statistical Model Checking (SMC), as a technique to mitigate the issue of state space explosion in numerical probabilistic model checking, can efficiently obtain an approximate result with an error bound by statistically analysing the simulation traces. SMC however may become very time consuming due to the generation of an extremely large number of traces in some cases. Improving the performance of SMC effectively is still a challenge. To solve the problem, we propose an optimized SMC approach called AL-SMC which effectively reduces the required sample traces, thus to improve the performance of SMC by automatic abstraction and learning. First, we present property-based trace abstraction for simplifying the cumbersome traces drawn from the original model. Second, we learn the analysis model called Prefix Frequency Tree (PFT) from the abstracted traces, and optimize the PFT using the two-phase reduction algorithm. By means of the optimized PFT, the original probability space is partitioned into several sub-spaces on which we evaluate the probabilities parallelly in the final phase. Besides, we analyse the core algorithms in terms of time and space complexity, and implement AL-SMC in our Modana Platform to support the automatic process. Finally we discuss the experiment results for the case study :energy-aware building which shows that the number of sample traces is effectively reduced (by nearly 20\% to 50\%) while ensuring the accuracy of the result with an acceptable error.     

多核系统动态温度管理TAPE策略的形式化验证

多核系统中,分布式DTM策略因其良好的可扩展性得到了广泛应用。在 部署分布式DTM策略前,必须验证其可靠性。为了克服传统分析方法的局限,模型检测技术被应用于分布式DTM策略的分析中。提出使用统计模型检测技术来验证多核系统中分布式DTM策略(以TAPE策略为例)的方案。使用UPPAAL SMC对TAPE策略的验证证明了TAPE策略的安全性、有效性、活性以及稳定性,从而验证DTM策略方案的可靠性。     

Application of bootstrap method in conservative estimation of reliability with limited samples

Accurate estimation of reliability of a system is a challenging task when only limited samples are available. This paper presents the use of the bootstrap method to safely estimate the reliability with the objective of obtaining a conservative but not overly conservative estimate. The performance of the bootstrap method is compared with alternative conservative estimation methods, based on biasing the distribution of system response. The relationship between accuracy and conservativeness of the estimates is explored for normal and lognormal distributions. In particular, detailed results are presented for the case when the goal has a 95% likelihood to be conservative. The bootstrap approach is found to be more accurate for this level of conservativeness. We explore the influence of sample size and target probability of failure on the quality of estimates, and show that for a given level of conservativeness, small sample sizes and low probabilities of failure can lead to a high likelihood of large overestimation. However, this likelihood can be reduced by increasing the sample size. Finally, the conservative approach is applied to the reliability-based optimization of a composite panel under thermal loading.     

ARINC653实时任务可调度性验证方法

针对综合模块化航空电子系统(Integrated Modular Avionics,IMA)存在周期任务和非周期任务,以及任务间依赖关系,传统方法不能准确验证其实时任务可调度性的问题,本文提出了一种基于Stopwatch时间自动机的ARINC653实时任务可调度性验证方法,利用模型检验工具UPPAAL对IMA系统进行建模仿真,并结合统计模型检验(Statistical Model Checking,SMC)与符号模型检验(Symbolic Model Checking,MC)来验证其可调度性。实验结果表明,该方法不仅快速验证了IMA系统的可调度性,而且能够准确定位不可调度任务。     

An efficient reliability analysis method combining adaptive Kriging and modified importance sampling for small failure probability

A vital challenge problem of structural reliability analysis is how to estimate the small failure probability with a minimum number of model evaluations. The Adaptive Kriging combined with Importance Sampling method (AK-IS) which is developed from the adaptive Kriging combined with Monte Carlo simulation (AK-MCS) is a viable method to deal with this challenge. The aim of this paper is to reduce the number of model evaluations of the existing AK-IS algorithm. Firstly, we use a contributive weight function to divide the candidate samples of model input variables generated in AK-IS. The candidate samples are used to select the best next sample to update the Kriging model in AK-IS. Secondly, select the best next sample only in the important area obtained according to the contributive weight value to failure probability to update the Kriging model until the stopping condition is satisfied. Thirdly, use the Kriging model constructed in the important area to predict the other area and update the important area by adding the point with the maximum contributive weight value in the area except the important area ceaselessly until the probability of the accurate identification on the limit state function’s signs (positive limit state value or negative limit state value) of all the importance sampling points satisfies a criterion. Finally, the updated Kriging model is used to estimate the failure probability especially for the small failure probability. The proposed method uses a thought from local to global in order to reduce the computational cost of AK-IS and simultaneously guarantees the accuracy of estimation. A non-linear oscillator system, a roof truss structure and a planar ten-bar structure are analyzed by the proposed method. The results demonstrate the efficiency and accuracy of the proposed method in structural reliability analysis especially for small failure probability.     

Statistical probabilistic model checking with a focus on time-bounded properties

Probabilistic verification of continuous-time stochastic processes has received increasing attention in the model-checking community in the past five years, with a clear focus on developing numerical solution methods for model checking of continuous-time Markov chains. Numerical techniques tend to scale poorly with an increase in the size of the model (the “state space explosion problem”), however, and are feasible only for restricted classes of stochastic discrete-event systems. We present a statistical approach to probabilistic model checking, employing hypothesis testing and discrete-event simulation. Since we rely on statistical hypothesis testing, we cannot guarantee that the verification result is correct, but we can at least bound the probability of generating an incorrect answer to a verification problem.     

多处理器实时系统可调度性分析的UPPAAL模型

随着多处理器实时系统在安全性攸关系统中的广泛应用,保证这类系统的正确性成为一项重要的工作.可调度性是实时系统正确性的一项关键性质.它表示系统必须满足的一些时间要求.传统的可调度性分析方法结论保守或者不完备,为了避免这些方法的缺陷,提出使用模型检测的方法来实现可调度性分析.提出了一个用于多处理器实时系统可调度性分析的模板,将与系统可调度性相关的部分包括实时任务、运行平台和调度管理模块都用时间自动机建模,并使用UPPAAL验证可调度的性质是否总被满足.符号化模型检测方法被用于推断可调度性,但是由于秒表触发的近似机制,符号化模型检测方法不能用于证明系统不可调度.作为补充,统计模型检测方法被用于估算系统不可调度的概率,并在系统不可调度时生成反例.此外,在系统可调度时,通过统计模型检测方法获取一些性能相关的信息.