利用形式化方法的机电系统 概率失效模式及影响分析
Probabilistic Failure Modes and Effects Analysis for Electromechanical Systems Based on Formal Method

针对传统的失效模式及影响分析中依靠领域专家分析判断系统单元失效与系统故障之间的关系,分析烦琐、容易出错且难以计算故障概率的问题,将形式化技术引入机电系统失效模式及影响分析中,提出了基于概率模型检测的机电系统概率失效模式及影响分析方法。基于机电系统中的状态变迁,研究了机电系统行为过程的随机模型及其形式化表达,建立了面向概率失效模式及影响分析的系统形式化随机模型;基于连续随机逻辑对系统的潜在故障进行了形式化规约,构建了潜在故障的概率形式化规约表达式;利用概率模型检测器对系统的随机模型和潜在故障进行形式化验证,从而辨识单元失效与系统潜在故障之间的关系,并自动计算单元失效所导致的系统故障概率,提高了失效模式与影响分析的准确性和效率。该方法不仅可以借助概率模型检测迅速准确地识别单元失效与系统潜在故障之间的因果关系,还可以自动计算系统故障概率。将该方法应用于数控机床进给系统,成功辨识出了限位开关失效所导致的系统故障并计算出了故障概率,从而验证了方法的可行性。
In conventional failure modes and effects analysis (FMEA), the relations between component failures and system faults are analyzed and determined by domain experts, which is tedious, error？？prone, and difficult to obtain the probabilities of the faults. In this paper, formal methods are introduced to FMEA for electromechanical systems and an approach to probabilistic FMEA (PFMEA) for electromechanical systems based on probabilistic model checking is proposed. Based on the state transitions in electromechanical systems, probabilistic model and its formal representation for the behavior process of the systems are studied and the formal probabilistic models for PFMEA are established. Continuous stochastic logic (CSL) formulas are employed to make formal specification of the potential faults in electromechanical systems, and the formal probabilistic specifications of potential fault are given. Formal verification is conducted for the system probabilistic models and potential faults, thereby the relations between the component failures and the potential system faults are identified. Moreover, the probabilities of the faults caused by component failures are calculated, so the efficiency and accuracy of the PFMEA are improved. By means of the approach presented in the paper, the causal relations between component failures and system faults are determined quickly and accurately, and the probabilities of the system faults are computed automatically. This approach is applied to the feed system of a CNC machine tool, and the system faults caused by limit switches and the probabilities of the faults are identified successfully, which demonstrates the feasibility of this approach