Model checking for survivability!
Model checking for survivability!
复制标题
模型检查生存能力！
DOI：
10.1109/qest.2005.21
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
B. Haverkort
中科院分区：
文献类型：
--
作者：
L. Cloth;B. Haverkort
商业和社会生活越来越依赖于大型通信和信息系统。自然灾害或有目的的攻击导致的部分或完全故障可能会产生严重影响。生存能力是指系统从此类灾难情况中恢复的能力。因此，评估生存能力应该是通信系统设计的重要组成部分。在本文中，我们采用模型检查方法来评估生存能力。我们使用逻辑 CSL 来精确地表达生存能力。系统操作通过标记的 CTMC 进行建模。然后模型检查算法可以自动决定系统是否具有生存能力。我们通过使用随机 Petri 网评估 Google 文件系统的生存能力来说明我们的方法。
Business and social life have become increasingly dependent on large-scale communication and information systems. A partial or complete breakdown as a consequence of natural disasters or purposeful attacks might have severe impacts. Survivability refers to the ability of a system to recover from such disaster circumstances. Evaluating survivability should therefore be an important part of communication system design. In this paper we take a model checking approach toward assessing survivability. We use the logic CSL to phrase survivability in a precise manner. The system operation is modelled through a labelled CTMC. Model checking algorithms can then decide automatically whether the system is survivable. We illustrate our method by evaluating the survivability of the Google file system using stochastic Petri nets.