Formally Verified On-Line Diagnosis
Formally Verified On-Line Diagnosis
复制标题
正式验证的在线诊断
DOI：
--
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
N. Suri
中科院分区：
文献类型：
--
作者：
C. Walter;P. Lincoln;N. Suri
可重构容错系统通过故障检测、故障隔离和重构来实现操作的可靠性属性，通常称为FDIR范式。故障诊断是该方法的关键组成部分，需要准确确定系统的健康状况和状态。不精确的状态评估可能会因乐观的诊断而导致灾难性的失败，或者相反，由于悲观的诊断而导致资源利用不足。与经典测试和其他离线诊断方法不同，我们开发了最大限度利用系统状态信息的程序，以提供持续的在线诊断和重新配置功能，作为系统操作的一个组成部分。与现有技术不同，我们的诊断方法不需要进行管理测试来收集综合症信息，而是基于监视冗余系统功能之间的系统消息流量。我们提供全面的在线诊断算法，能够处理节点和链路级别不同严重程度的连续故障。所提出的算法不仅本质上是在线的，而且本身能够容忍诊断过程中的错误。对所有提出的算法进行了形式分析。这些证明既提供了对算法操作的深入了解，也有助于对所开发的算法进行严格的形式验证。
A reconfigurable fault tolerant system achieves the attributes of dependability of operations through fault detection, fault isolation and reconfiguration, typically referred to as the FDIR paradigm. Fault diagnosis is a key component of this approach, requiring an accurate determination of the health and state of the system. An imprecise state assessment can lead to catastrophic failure due to an optimistic diagnosis, or conversely, result in underutilization of resources because of a pessimistic diagnosis. Differing from classical testing and other off-line diagnostic approaches, we develop procedures for maximal utilization of the system state information to provide for continual, on-line diagnosis and reconfiguration capabilities as an integral part of the system operations. Our diagnosis approach, unlike existing techniques, does not require administered testing to gather syndrome information but is based on monitoring the system message traffic among redundant system functions. We present comprehensive on-line diagnosis algorithms capable of handling a continuum of faults of varying severity at the node and link level. Not only are the proposed algorithms on-line in nature, but are themselves tolerant to faults in the diagnostic process. Formal analysis is presented for all proposed algorithms. These proofs offer both insight into the algorithm operations and facilitate a rigorous formal verification of the developed algorithms.