• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Computer Science and Information Systems >Formal Verification of Signature-monitoring Mechanisms by Model Checking
【24h】

Formal Verification of Signature-monitoring Mechanisms by Model Checking

机译：通过模型检查对签名监视机制进行形式验证

获取原文
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

In recent decades, reliability in the presence of transient faults has been a significant problem. To mitigate the effects of transient faults, fault-tolerant techniques are proposed. However, validating the effectiveness of fault-tolerant techniques is another problem. In this paper, we present an original approach to evaluate the effectiveness of signature-monitoring mechanisms. The approach is based on model-checking principles. First, the fault tolerant model is proposed using step-operational semantics. Second, the fault model is refined into a state transition system that is translated into the input program of the symbolic model checker NuSMV. Using NuSMV, two reprehensive signature-monitoring algorithms are verified. The approach avoids the state space explosion problem and the verification was completed with practical time. The verification results reveal some undetected errors, which have not been previously observed.
机译：在最近的几十年中，在存在瞬时故障的情况下的可靠性一直是一个重大问题。为了减轻瞬态故障的影响，提出了容错技术。但是，验证容错技术的有效性是另一个问题。在本文中，我们提出了一种评估签名监视机制有效性的原始方法。该方法基于模型检查原理。首先，使用逐步操作语义提出了容错模型。其次，将故障模型提炼为状态转换系统，然后将其转换为符号模型检查器NuSMV的输入程序。使用NuSMV，验证了两种全面的签名监视算法。该方法避免了状态空间爆炸问题，并且验证是在实际时间内完成的。验证结果显示了一些未发现的错误，这些错误以前没有被观察到。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号