作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程 ›› 2012, Vol. 38 ›› Issue (17): 38-41. doi: 10.3969/j.issn.1000-3428.2012.17.011

• 软件技术与数据库 • 上一篇    下一篇

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

周清雷,张 兵,席 琳   

  1. (郑州大学信息工程学院,郑州 450052)
  • 收稿日期:2011-09-28 修回日期:2012-01-02 出版日期:2012-09-05 发布日期:2012-09-03
  • 作者简介:周清雷(1962-),男,教授、博士生导师、CCF高级会员,主研方向:模型检测,形式化方法,信息安全;张 兵、席 琳,博士研究生
  • 基金资助:
    国家“863”计划基金资助项目“基于ASP模式的软件服务支持技术研究”(2007AA010408)

System Survivability Analysis Based on Model Checking

ZHOU Qing-lei, ZHANG Bing, XI Lin   

  1. (School of Information Engineering, Zhengzhou University, Zhengzhou 450052, China)
  • Received:2011-09-28 Revised:2012-01-02 Online:2012-09-05 Published:2012-09-03

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

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

Abstract: 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.

Key words: survivability analysis, formal method, model checking, PRISM checking tool\ discrete Markov chain, probability computation tree logic

中图分类号: