Model checking for fault explanation Conference

Jiang, S, Fuhrman, TE, Jha, SK. (2006). Model checking for fault explanation . 2012 IEEE 51ST ANNUAL CONFERENCE ON DECISION AND CONTROL (CDC), 404-409. 10.1109/cdc.2006.377556

cited authors

  • Jiang, S; Fuhrman, TE; Jha, SK

authors

abstract

  • Model checking is very effective at finding out even subtle faults in system designs. A counterexample is usually generated by model checking algorithms when a system does not satisfy the given specification. However, a counterexample is not always helpful in explaining and isolating faults in a system when the counterexample is very long, which is usually the case for large scale systems. As such, there is a pressing need to develop fault explanation and isolation techniques. In this paper, we present a new approach for the fault explanation and isolation in discrete event systems with LTL (linear-time temporal logic) specifications. The notion of fault seed is introduced to characterize the cause of a fault. The identification of the fault seed is further reduced to a model checking problem. An algorithm is obtained for the fault seed identification. An example is provided to demonstrate the effectiveness of the approach developed. © 2006 IEEE.

publication date

  • January 1, 2006

published in

Digital Object Identifier (DOI)

start page

  • 404

end page

  • 409