基于模型检测的机电系统FMEA研究

Study on FMEA for Electromechanical Systems Based on Model Checking

失效模式与影响分析(Failure modes and effects analysis,FMEA)是一种重要的设计评审和可靠性评估手段,但传统FMEA是非形式化的,分析烦琐且容易出错。将形式化技术引入机电系统FMEA,提出基于模型检测的机电系统FMEA方法。基于机电系统中的状态和事件,研究机电系统行为过程的形式化建模,针对单元失效建立面向FMEA的系统形式化模型;基于计算树逻辑(Computation tree logic,CTL)对机电系统的潜在故障进行形式化规约,并以潜在故障的否定命题构建待验证的系统行为属性;借助于模型检测工具遍历系统状态空间来检验系统是否满足行为属性,从而辨识系统单元失效与系统潜在故障之间的关系,实现基于模型检测的机电系统FMEA;将上述方法应用到数控机床进给系统,通过模型检测成功辨识出限位开关失效所导致的系统故障,验证了该方法的可行性。

Failure modes and effects analysis（FMEA） is an important means of design review and reliability evaluation, but conventional FMEA is tedious and error-prone due to its informalization. Formal methods are introduced to FMEA for electromechanical systems and an approach to FMEA for electromechanical systems based on model checking is proposed. Based on the states and events in electromechanical systems, formal modeling for the behavior process of the systems is studied and formal model for FMEA with respect to component failures is established. Computation tree logic（CTL） formulas are employed to make formal specification of the potential faults in electromechanical systems, and the negative propositions of potential fault are used to form system properties to be verified. By traversing system space, a system is checked if it satisfies the system properties and thereby the relations between component failures and the system potential faults are identified, so model checking based FMEA for electromechanical systems is realized. The above approach is applied to feed system of a CNC machine tool, and the system faults caused by limit switches are identified successfully, which demonstrates the feasibility of the proposed approach.