摘要
由于定量信息和非线性因果关系的丢失,符号有向图(SDG)的故障诊断解需要进一步进行校核与验证.将SDG故障诊断解的验证置于符号模型检测框架中进行研究,提出了基于符号模型检测的SDG故障诊断解形式化验证方法.首先定义了SDG模型的有限状态变迁系统形式化描述,建立了符号模型检测(SMV)模型;其次引入故障传播时间定义了模型观测变量的动态验证信息,提出了基于步进式监控的动态推理验证策略;然后扩展了动态推理验证过程的SMV模型,提出了验证算法SSDGFD SMC;最后,通过一个简单贮水罐系统的SDG模型实例验证了算法SSDGFD SMC的有效性.
Due to drop of quantitative and nonlinear causal information,the solution of signed directed graph（SDG） fault diagnosis needs to be further verified and validated.Verification for the solution of SDG fault diagnosis is placed in the framework of symbolic model checking.A formal verification approach for the solution of SDG fault diagnosis via symbolic model checking（SSDGFD SMC） is proposed.A formal characterization of SDG model,as a finite state transition system,is defined firstly,and SMV（symbolic model verifier） module is modeled.Secondly,the dynamic verification information for the observed variables is set up by means of fault propagation time,and the dynamic inference verification strategy based on progressive monitoring is analyzed.Then SMV model is extended for the dynamic inference verification process,and SSDGFD SMC algorithm is designed.Finally,the practical applicability of SSDGFD SMC is demonstrated by a simple water tank SDG model.
出处
《信息与控制》
CSCD
北大核心
2010年第4期423-429,共7页
Information and Control
基金
国家自然科学基金资助项目(6080503860725309)
国家863计划资助项目(2006AA04Z258)
关键词
SDG模型
符号模型检测
动态验证信息
动态验证策略
SDG model
symbolic model checking
dynamic verification information
dynamic verification strategy
