概率行为树模型转化为模型检测模型方法研究

Research on Conversion from Probabilistic Behavior Tree Model to Formal Model of Model Checking

将概率模型检测方法运用到机电系统可靠性评价中,可以有效提高可靠性分析特别是FMEA分析的准确性与效率。利用概率模型检测对机电系统进行可靠性评价需要对机电系统进行形式化建模,直接利用模型检测语言对系统进行形式化建模直观性较差,建模难度大。对机电系统的概率行为树建模进行了介绍,分析了概率模型检测工具PRISM提供的形式化建模语言,定义了从概率行为树模型到PRISM形式化模型的转换规则,实现了机电系统概率行为树模型向模型检测形式化模型的转换。以数控机床工作台系统为例验证了转换方法的可行性。

Applying the method of probability model checking to reliability evaluation of electromechanical systems can improve the accuracy and efficiency of reliability analysis,especially FMEA. Reliability evaluation based on model checking needs formal modeling of electromechanical systems,however it’s hard and not intuitive to model a system directly by the modeling language of model checker. Modeling electromechanical systems with probabilistic behavior trees is introduced,and formal modeling language provided by model checker PRISM is analyzed. Conversion rules from probabilistic behavior tree model to PRISM model are defined. The conversion from probabilistic behavior tree model to the formal model of model checking for electromechanical systems is realized by means of the rules. A workbench system of CNC machine tool is given to demonstrate the feasibility of the proposed conversion rules.