首页> 外文期刊>International journal of critical computer-based systems >Formal verification of intermittent fault diagnosability of discrete-event systems using model-checking
【24h】

Formal verification of intermittent fault diagnosability of discrete-event systems using model-checking

机译:使用模型检查的离散事件系统间歇性故障可诊断性的形式验证

获取原文
获取原文并翻译 | 示例
           

摘要

Fault diagnosis of complex and dynamic systems is a crucial and challenging task, essentially with respect to guaranteeing the reliable, safe and efficient operation of such systems. Most research in this field has been focused on permanent failure diagnosis, i.e., once a fault occurs, the system remains indefinitely faulty. However, experience with fault diagnosis in real-life systems shows that intermittent faults, i.e., faults that can be automatically recovered, are predominant and are among the most challenging kinds of faults to detect and isolate. In this paper, we address the formal verification of intermittent fault diagnosability in discrete-event systems. The system is modelled by a finite state automaton and intermittent faults are defined as faults that can automatically recover once they have occurred. Two definitions of diagnosability, regarding the detection of fault occurrence within a finite delay and the detection of fault occurrence before its recovery, are discussed. The diagnosability is analysed on the basis of the twin-plant structure, which is encoded as a Kripke structure, while diagnosability conditions are formulated using LTL temporal logic.
机译:复杂且动态系统的故障诊断是一项至关重要且具有挑战性的任务,实质上是在保证此类系统的可靠,安全和有效运行方面。该领域中的大多数研究都集中在永久性故障诊断上,即,一旦发生故障,系统将无限期地保持故障状态。但是,在实际系统中进行故障诊断的经验表明,间歇性故障(即可以自动恢复的故障)占主导地位,并且是要检测和隔离的最具挑战性的故障之一。在本文中,我们解决了离散事件系统中间歇性故障可诊断性的形式验证。该系统由有限状态自动机建模,间歇性故障定义为一旦发生就可以自动恢复的故障。讨论了可诊断性的两种定义,即在有限延迟内检测故障发生和在故障恢复之前检测故障发生。基于双工厂结构(被编码为Kripke结构)对可诊断性进行了分析,而可诊断性条件则使用LTL时间逻辑来制定。

著录项

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号