An Approach to Post Mortem Diagnosability Analysis for Interacting Finite State Systems

We present a model based approach to diagnosability analysis for interacting finite state systems where fault isolation is deferred until the system comes to a standstill. Local abstractions of the system model are used to alleviate the state space explosion. Pairs of closely coupled automata are merged and replaced by a single automaton with an equivalently behavior as seen from the rest of the system; interaction between the merged automata is internalized and the new equivalent automaton is subsequently abstracted from internal behavior irrelevant to fault isolation. In moderately concurrent systems these steps can often be iterated until the system consists of a single automaton providing a compact encoding of all possible fault scenarios of the original model. We illustrate how the resulting abstraction can be used as a basis for post mortem diagnosability analysis.