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

• 作者: 王健 王慧强 赵国生
• 来源期刊: 高技术通讯
• 学科: 工学
• 关键词: 生存性 概率模型检测 形式化规约 任务关键系统 量化分析
• 年，卷（期）: 2009,（6）
• 所属期刊栏目: 计算机与通信技术
• 页码范围: 572-579
• 页数: 8页
• 分类号: TP3
• 字数: 5559字
• 语种: 中文
• DOI: 10.3772/j.issn.1002-0470.2009.06.004

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王慧强	哈尔滨工程大学计算机科学与技术学院	159	1573	20.0	32.0
2	王健	哈尔滨工程大学计算机科学与技术学院	133	1512	18.0	34.0
3	赵国生	哈尔滨工程大学计算机科学与技术学院	14	165	7.0	12.0