分布式任务关键系统生存性自动分析与验证

摘要

提出了一种应用概率模型检测技术进行分布式任务关键系统生存性的量化分析研究方法.该方法对攻击者和系统的交互行为进行精简抽象,在此基础上使用PRISM高级语言构造连续时间马尔可夫链系统概率模型.针对不同程度的攻击故障及系统服务水平,以连续随机逻辑建立系统生存性的形式化规约.借助概率模型检测工具PRISM对模型进行统计和验证,并图形化地表示出系统生存性的自动分析结果.理论分析和实验结果验证了上述方法的合理性和有效性,这些结果可在理论上指导可生存系统的设计和实现.%The paper proposes a method for guantitative analysis of the survivability of distributed mission-critical systems based on the probabilistic model checking technology. The method abstracts the interactive behaviors between intruders and the system, and constructs the continuous-time Markov chains probabilistic model of the system using the PRISM language, then identifies the formal specification for the system survivability by continuous stochastic logic aiming at different disaster degrees and service levels, and ultimately, analyzes the model statistically and validates the model with the probabilistic model checking tool PRISM, and graphically demonstrates the automated analysis results of the system's survivability. The results of the theoretical analysis and the experiment show the proposed method's rationality and effectiveness. These conclusions can help to direct the design and implementation of survivable systems.