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

doi:10.3969/j.issn.1000-3428.2012.17.011

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

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

周清雷，张兵，席琳

(郑州大学信息工程学院，郑州 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

(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

摘要/Abstract

摘要： 提出一种采用模型检测进行系统生存性分析的形式化方法。给出系统所处环境及主要提供的服务，引入灾难和错误等因素，建立系统生存性模型。通过描述系统的可生存能力，确定其生存性需求并转换为相应的逻辑表示。以电话接入网络为例，利用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

中图分类号:

TP301

周清雷, 张兵, 席琳. 基于模型检测的系统生存性分析[J]. 计算机工程, 2012, 38(17): 38-41.

ZHOU Qing-Lei, ZHANG Bing, XI Lin. System Survivability Analysis Based on Model Checking[J]. Computer Engineering, 2012, 38(17): 38-41.

https://www.ecice06.com/CN/Y2012/V38/I17/38

参考文献

[1] Moitra S D, Konda S L. A Simulation Model for Managing Survivability of Networked Information Systems[R]. Pittsburgh, USA: [s. n.], Tech. Rep.: CMU/SEI-2000-TR-020, 2000.
[2] Wang Chunlei, Wang Dongxia, Dai Yiqi. Towards a Unified Framework for Network Survivability Measurement[C]//Proc. of the 2nd International Conference on Networks Security, Wireless Communications and Trusted Computing. Wuhan, China: [s. n.], 2010.
[3] Chen Shanzhi, Cheng Shiduan. Survivability Strategies for the Future Chinese SDH Transport Network[C]//Proc. of ICCT’96. [S. l.]: IEEE Press, 1996.
[4] Tipper D, Dahlberg T, Shin H. Providing Fault Tolerance in Wireless Access Networks[J]. IEEE Communications Magazine, 2002, 40(1): 58-64.
[5] Zolfaghari A, Kaudel F J. Framework for Network Survivability Performance[J]. IEEE Journal on Select Areas in Communications, 1994, 12(1): 46-51.
[6] Patrl J K, Kim S U, Su D H. A Framework for Managing Faults and Attacks in All-optical Transport Networks[C]//Proc. of DISCEX II’01. [S. l.]: IEEE Press, 2001.
[7] 张慧敏, 古天龙. 基于Petri网模型的Ad Hoc网络可生存性分析[J]. 系统仿真学报, 2008, 20(8): 2487-2490.
[8] 王海泉, 马心意, 夏春和. 一种MANET可生存性模型建模方法[J]. 信息安全与通信保密, 2010, (1): 88-92.
[9] 陈建辉, 王文义, 朱维军. 一种基于并发命题投影时序逻辑模型检测的入侵检测方法[J]. 计算机科学, 2010, 37(10): 116-117.
[10] 林惠民, 张文辉. 模型检测: 理论、方法与应用[J]. 电子学报, 2002, 30(12): 1907-1912.
[11] Knight J, Sullivan K. On the Definition of Survivability[Z]. 2000.
[12] Kwiatkowska M, Norman G, Sproston J, et al. Symbolic Model Checking for Probabilistic Timed Automata[J]. Information and Computation, 2007, 205(7): 1027-1077.
[13] Laroussinie F, Markey N, Schnoebelen P. Model Checking Timed Automata with One or Two Clocks[C]//Proc. of CONCUR’04. [S. l.]: Springer, 2004.
[14] Jha S, Wing J, Linger R, et al. Survivability Analysis of Network Specifications[C]//Proc. of DSN’00. [S. l.]: IEEE Press, 2000.
[15] Kwiatkowska M. Model Checking for Probability and Time: From Theory to Practice[C]//Proc. of the 18th Annual IEEE Symposium on Logic in Computer Science. [S. l.]: IEEE Press, 2003.
[16] Liu Yun, Mendiratta V B, Trivedi K S. Survivability Analysis of Telephone Access Network[C]//Proc. of the 15th International Symposium on Software Reliability Engineering. [S. l.]: IEEE Press, 2004.
[17] PRISM[EB/OL]. (2010-05-18). http://www.prismmodelchecker. org.

选择文件类型/文献管理软件名称

选择包含的内容

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

System Survivability Analysis Based on Model Checking

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价

[1]	谢娜, 谭文安, 曹彦, 赵璐. 移动边缘计算中安全信息流建模与分析[J]. 计算机工程, 2022, 48(5): 35-42,52.
[2]	闫倩倩, 缪炜恺. 轨道交通控制软件中基于场景的需求分析方法[J]. 计算机工程, 2021, 47(8): 284-293,300.
[3]	刘阳, 高世国. 基于随机模型检验的社交网络隐私保护研究[J]. 计算机工程, 2021, 47(5): 144-153.
[4]	杨锦翔, 熊焰, 黄文超. 基于强化学习的安全协议形式化验证优化研究[J]. 计算机工程, 2021, 47(12): 141-146.
[5]	陈金鑫,苏雯. 基于Event-B的自动化模块组合方法研究[J]. 计算机工程, 2019, 45(5): 298-307,314.
[6]	任胜兵,张健威,吴斌,王志健. Spark环境下基于SMT的分布式限界模型检测[J]. 计算机工程, 2017, 43(6): 19-23,29.
[7]	唐郑熠,王金水,何栋炜,薛醒思,胡文瑜. 馈线自动化算法的形式化建模与验证[J]. 计算机工程, 2016, 42(3): 89-93.
[8]	陈永,张薇,胡晓辉. 基于改进EventB建模的高速列车追踪运行仿真研究[J]. 计算机工程, 2015, 41(8): 256-261.
[9]	赵璐,张健沛,杨静. 收缩候选回溯集的有状态动态偏序归约方法[J]. 计算机工程, 2015, 41(5): 70-76.
[10]	许兴旺,骆翔宇. 基于MAS 模型检测与抽象的Web 服务验证[J]. 计算机工程, 2015, 41(3): 26-31,36.
[11]	劳佳琪,文中华,伍小辉,唐杰. 一种快速求强规划解的算法[J]. 计算机工程, 2015, 41(3): 162-166.
[12]	龙凤,文中华,唐杰,王进宗. 不确定规划中可达关系的快速求解算法[J]. 计算机工程, 2015, 41(1): 196-199.
[13]	伍小辉,文中华,李洋,劳佳琪. 不确定规划中的多Agent带权值强规化算法[J]. 计算机工程, 2015, 41(1): 190-195.
[14]	余莹. 组合服务交互测试研究综述[J]. 计算机工程, 2013, 39(5): 78-83.
[15]	董昱, 水晶, 黎磊. CTCS-2级列控系统的形式化建模与验证[J]. 计算机工程, 2013, 39(3): 12-15.

模态框（Modal）标题

选择文件类型/文献管理软件名称

选择包含的内容

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

System Survivability Analysis Based on Model Checking

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价