机电系统的概率行为树建模及可靠性评价

直接利用模型检测工具提供的形式化语言对系统进行形式化建模直观性较差、建模难度大，因此利用概率行为树对机电系统进行形式化建模，并通过概率模型检测对机电系统进行可靠性评价。对机电系统功能执行过程中功能载体的状态及其变迁进行了研究。基于概率行为树的语义和句法，提出了机电系统状态变迁过程的概率行为树建模方法，开发了建模支持工具。利用该建模工具可实现机电系统的概率行为树建模并能将其转换为基于PRISM语言的形式化模型。基于机电系统的潜在故障，用连续随机逻辑对机电系统可靠性评价指标进行形式化规约。基于概率行为树模型和可靠性评价指标的形式化规约，利用模型检测工具PRISM实现了对机电系统的可靠性评价。该方法比直接使用形式化语言建模更直观、易于理解和掌握。

Modeling and Reliability Evaluation for Electromechanical Systems Based on Probabilistic Behavior Trees

Modeling systems directly using formal language provided by model checker were non-intuitive and difficult. Therefore, probabilistic behavior trees were introduced to model the electromechanical systems and evaluate their reliability through probabilistic model checking herein. States and transitions of function carriers in the function execution of electromechanical systems were studied. Based on the syntax and semantics of probabilistic behavior trees, an approach was proposed to model the state transition of electromechanical systems by probabilistic behavior trees. A support tool for probabilistic behavior tree modeling was developed, which could establish the model of electromechanical systems with probabilistic behavior trees and translate the model into the formal model based on PRISM codes. Based on the potential faults in electromechanical systems, continuous stochastic logic formulas were employed to specify the reliability evaluation indices formally. With the probabilistic behavior tree model and formal specification of reliability evaluation indices, reliability evaluation was implemented using probabilistic model checker PRISM. Compared with the modeling method using formal language directly, the method presented herein is more intuitive, easier to understand and use.