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

System Survivability Analysis Based on Model Checking

作　　者：周清雷[1] 张兵[1] 席琳[1] 

机构地区：[1]郑州大学信息工程学院,郑州450052

出　　处：《计算机工程》2012年第17期38-41,共4页Computer Engineering

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

摘　　要：提出一种采用模型检测进行系统生存性分析的形式化方法。给出系统所处环境及主要提供的服务,引入灾难和错误等因素,建立系统生存性模型。通过描述系统的可生存能力,确定其生存性需求并转换为相应的逻辑表示。以电话接入网络为例,利用PRISM对系统进行建模及验证,结果表明,该形式化方法可以规范并简化生存性分析过程。This paper presents a formal method based on the model checking to analyze the survivability. On the basis of giving system environment and the main services, the survivability system is modeled on introducing the factors of disaster and error. The system＇s survivability requirement is determined and converted to the modal logic. It takes the telephone access network as an example, the method is implemented by the PRISM, and results show that the model checking can regulate, and simplify the survivability analysis process.

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]