Florida International University
Edit Your Profile
FIU Discovery
Toggle navigation
Browse
Home
People
Organizations
Scholarly & Creative Works
Research Facilities
Support
Edit Your Profile
Model checking for fault explanation
Conference
Jiang, S, Fuhrman, TE, Jha, SK. (2006). Model checking for fault explanation .
404-409. 10.1109/cdc.2006.377556
Share this citation
Twitter
Email
Jiang, S, Fuhrman, TE, Jha, SK. (2006). Model checking for fault explanation .
404-409. 10.1109/cdc.2006.377556
Copy Citation
Share
Overview
Identifiers
Additional Document Info
View All
Overview
cited authors
Jiang, S; Fuhrman, TE; Jha, SK
authors
Jha, Sumit Kumar
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
Identifiers
Digital Object Identifier (DOI)
https://doi.org/10.1109/cdc.2006.377556
International Standard Book Number (ISBN) 10
1424401712
International Standard Book Number (ISBN) 13
9781424401710
Additional Document Info
start page
404
end page
409