Abstract:

Because of quantitative and nonlinear causal information, diagosability of the signed directed graph(SDG) model needs to be further verified and validated. A formal verification approach to diagnosability via symbolic model checking is proposed. A formal characterization of SDG, as a finite state transition system, is transformed firstly, and a symbolic model verifier (SMV) module is modeled. In the framework of the finite state transition system, a diagnosis function is established, and then the diagnosable definition of a diagnosis condition is defined using the idea of diagnosis context. By means of NuSMV, a coupled SMV module is constructed, and then the SDGD_CSMV algorithm is designed with the computation temporal logic (CTL) definition of diagnosable property. Finally, the practical applicability within a simple water tank SDG model is demonstrated, which proves the validation of the diagnosable definition and SDGD_CSMV.