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

摘要：

提出了一种应用概率模型检测技术进行分布式任务关键系统生存性的量化分析研究方法.该方法对攻击者和系统的交互行为进行精简抽象,在此基础上使用PRISM高级语言构造连续时间马尔可夫链系统概率模型.针对不同程度的攻击故障及系统服务水平,以连续随机逻辑建立系统生存性的形式化规约.借助概率模型检测工具PRISM对模型进行统计和验证,并图形化地表示出系统生存性的自动分析结果.理论分析和实验结果验证了上述方法的合理性和有效性,这些结果可在理论上指导可生存系统的设计和实现.

关键词：生存性、概率模型检测、形式化规约、任务关键系统、量化分析

所属期刊栏目：19

分类号：TP3;U4

资助基金：863计划2007AA01Z401;国家自然科学基金90718003

在线出版日期：2009-09-24（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：572-579