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

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

System Survivability Analysis Based on Model Checking

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.