基于模型检测的系统生存性分析

摘要：

提出一种采用模型检测进行系统生存性分析的形式化方法.给出系统所处环境及主要提供的服务,引入灾难和错误等因素,建立系统生存性模型.通过描述系统的可生存能力,确定其生存性需求并转换为相应的逻辑表示.以电话接入网络为例,利用PRISM对系统进行建模及验证,结果表明,该形式化方法可以规范并简化生存性分析过程.

关键词：生存性分析、形式化方法、模型检测、PRISM检测工具、离散马尔科夫链、概率计算树逻辑

所属期刊栏目：38

分类号：TP301(计算技术、计算机技术)

资助基金：国家“863”计划基金资助项目“基于ASP模式的软件服务支持技术研究”2007AA010408

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

页数：共4页

页码：38-41