摘要
提出了一种应用概率模型检测技术进行分布式任务关键系统生存性的量化分析研究方法。该方法对攻击者和系统的交互行为进行精简抽象,在此基础上使用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 disas- ter degrees and service levels, and ultimately, analyzes the model statistically and validates the model with the probabilis- tic 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.
出处
《高技术通讯》
EI
CAS
CSCD
北大核心
2009年第6期572-579,共8页
Chinese High Technology Letters
基金
863计划(2007AA01Z401)
国家自然科学基金(90718003)资助项目
关键词
生存性
概率模型检测
形式化规约
任务关键系统
量化分析
survivability, probabilistic model checking, formal specification, mission-critical systems, quantitative analysis
