• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>IFAC PapersOnLine >Is LTL model-checking effective for Diagnosability Verification? ?
【24h】

Is LTL model-checking effective for Diagnosability Verification? ?

机译：是LTL模型检查有效可诊断验证吗？ ？

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

摘要

In this work we propose a model checking approach to deal with the problem of the diagnosability verification. In this approach we consider the normal and the faulty behavior of a transition system (TS). We describe the diagnosability property by using an unique linear temporal logic (LTL) formula. Using LTL model checking we can test if the system is not diagnosable if it does not satisfy our proposed LTL-formula. Our approach can be carried out in SPIN model checker which is a tool used for formal verification of models. One advantage of SPIN is that it can handle a large state space which can be useful for diagnosability verification of complex system. We illustrate the effectiveness of our approach by means of a scalable benchmark of a railway level crossing system for n tracks and compare the results found with the ones found using typical tools for verification of diagnosability of Discrete Event Systems (DES).
机译：在这项工作中，我们提出了一种模型检查方法来处理诊断验证问题。在这种方法中，我们考虑过渡系统（TS）的正常和故障行为。我们使用唯一的线性时间逻辑（LTL）公式来描述诊断属性。使用LTL模型检查如果在不满足我们所提出的LTL公式的情况下，我们可以测试系统是否无法诊断。我们的方法可以在旋转模型检查器中进行，该方法是用于正式验证模型的工具。旋转的一个优点是它可以处理大状态空间，这对于复杂系统的诊断验证是可用的。我们通过用于N轨道的铁路级交叉系统的可扩展基准来说明我们方法的有效性，并比较使用典型工具找到的结果，用于验证离散事件系统（des）的诊断。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号