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

doi:10.3969/j.issn.1004-132X.2020.14.001

摘要/Abstract

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

关键词: 概率行为树, 概率模型检测, 可靠性评价, 机电系统

Abstract: 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.

Key words: probabilistic behavior tree, probabilistic model checking, reliability evaluation, electromechanical system

中图分类号:

TH122

杨培林, 刘青, 樊娟妮, 侯翌. 机电系统的概率行为树建模及可靠性评价[J]. 中国机械工程, 2020, 31(14): 1639-1646.

YANG Peilin, LIU Qing, FAN Juanni, HOU Yi. Modeling and Reliability Evaluation for Electromechanical Systems Based on Probabilistic Behavior Trees[J]. China Mechanical Engineering, 2020, 31(14): 1639-1646.

参考文献

[1] 贾利民, 林帅. 系统可靠性方法研究现状与展望[J]. 系统工程与电子技术, 2015, 37(12):2887-2893. JIA Limin, LIN Shuai. Current Status and Prospect for the Methods of System Reliability[J]. Systems Engineering and Electronics, 2015, 37(12):2887-2893.
[2] SACHDEVA A,KUMAR D, KUMAR P. Reliability Analysis of Pulping System Using Petri Nets[J]. International Journal of Quality and Reliability Management, 2008, 25(8):860-876.
[3] 沈戈, 苏春, 许映秋. 基于Petri网理论的动态系统可靠性建模方法研究[J]. 机械工程与自动化, 2006, 2:1-3. SHEN Ge, SU Chun, XU Yingqiu. Research on the Method of Reliability Analysis for Dynamic System Based on Petri Net[J]. Mechanical Engineering & Automation, 2006, 2:1-3.
[4] 苏春. 基于GSPN模型的系统动态可靠性仿真研究[J].中国机械工程, 2008, 19(1):1-5. SU Chun. Simulation Research on System Dynamic Reliability Based on General Stochastic Petri Net[J]. China Mechanical Engineering, 2008, 19(1):1-5.
[5] 石健, 王少萍, 王康. 基于GSPN的机载液压作动系统可靠性模型[J]. 航空学报, 2011, 32(5):920-933. SHI Jian, WANG Shaoping, WANG Kang. GSPN-based Reliability Model of Aircraft Hydraulic Actuator System[J].Acta Aeronautica et Astronautica Sinica, 2011, 32(5):920-933.
[6] MATSUOKA T, KOBAYASHI M. GO-FLOW:A New Reliability Analysis Methodology[J]. Nuclear Science and Engineering, 1989, 98(1):64-78.
[7] 沈祖培, 黄祥瑞. GO法原理及应用[M]. 北京:清华大学出版社, 2004. SHEN Zupei, HUANG Xiangrui. Principle and Application of GO Methodology[M]. Beijing:Tsinghua University Press, 2004.
[8] GRUNSKE L, COLVIN R, WINTER K. Probabilistic Model-checking Support for FMEA[C]//Proceedings of the Fourth International Conference on Quantitative Evaluation of Systems. Edinburgh:IEEE, 2007:119-128.
[9] ALJAZZAR H, FISCHER M, GRUNSKE L, et al. Safety Analysis of an Airbag System Using Probabilistic FMEA and Probabilistic Counterexamples[C]//Proceedings of the 2009 Sixth International Conference on the Quantitative Evaluation of Systems. Budapest:IEEE, 2009:299-308.
[10] KWIATKOWSKA M, NORMAN G, PARKER D. Controller Dependability Analysis by Probabilistic Model Checking[C]//Proceedings of 13th IFAC Symposium on Information Control Problems in Manufacturing. Amsterdam:Elsevier, 2004:112-119.
[11] OLIVERA P, HANS-DIETER E. Model Checking PLC Software Written in Function Block Diagram[C]//Proceedings of the 2010 Third International Conference on Software Testing, Verification and Validation. Paris:IEEE, 2010:439-448.
[12] 杨培林,徐凯,薛冲冲,等. 基于模型检测的机电系统FMEA研究[J]. 机械工程学报, 2016, 52(16):162-168. YANG Peilin, XU Kai, XUE Chongchong, et al. Study on FMEA for Electromechanical Systems Based on Model Checking[J]. Journal of Mechanical Engineering, 2016, 52(16):162-168.
[13] 林惠民,张文辉. 模型检测:理论、方法与应用[J].电子学报, 2002,30(12A):1907-1912. LIN Huimin, ZHANG Wenhui. Model Checking:Theories,Technigues and Applications[J]. Acta Electronica Sinica, 2002,30(12A):1907-1912.
[14] HORSTE M M Z, SCHNIEDER E. Modelling Train Control Systems with Petri Nets:a Functional Reference Architecture[C]//Proceedings on 2000 IEEE International Conference on Systems, Man & Cyberbetics. Nashville:IEEE, 2000:3081-3086.
[15] 张国印, 刘铭, 姚爱红,等.基于扩展Petri网的系统建模及形式化验证方法[J].计算机应用研究,2010,27(12):4587-4590. ZHANG Guoyin, LIU Ming, YAO Aihong, et al. Methodology of Modeling and Formal Verification Based on Extended Petri Net[J]. Application Research of Computers, 2010, 27(12):4587-4590.
[16] 李震,刘斌,李小勋,等.基于Petri网模型检验的安全关键软件需求验证[J].系统工程与电子技术,2011,33(2):458-463. LI Zhen, LIU Bin, LI Xiaoxun, et al. Verification of Safety Critical Software Requirement Based on Petri-net Model Checking[J]. Journal of Systems Engineering and Electronics, 2011,33(2):458-463.
[17] DROMEY R G. From Requirements to Design:Formalizing the Key Steps[C]//Proceedings of First International Conference on Software Engineering and Formal Methods. Brisbane:IEEE, 2003:2-13.
[18] LINDSAY P A. Behavior Trees:from Systems Engineering to Software Engineering[C]//Proceedings of the 20108th IEEE International Conference on Software Engineering and Formal Methods. Pisa:IEEE, 2010:21-30.
[19] GRUNSKE L, WINTER K, COLVIN R. Timed Behavior Trees and Their Application to Verifying Real-time System[C]//Proceedings of the 2007 Australian Software Engineering Conference. Melbourne:IEEE, 2007:211-222.
[20] COLVIN R, GRUNSKE L, WINTER K. Probabilistic Timed Behavior Trees[C]//Proceedings of the 6th International Conference on Integrated Formal Methods. Berlin:Springer, 2007:156-175.
[21] COLVIN R, GRUNSKE L, WINTER K. Timed Behavior Trees for Failure Mode and Effects Analysis of Time-critical Systems[J]. The Journal of Systems and Software, 2008, 81:2163-2182.
[22] 熊海军,朱永利,赵建利,等. 基于行为树的协议建模方法及其应用研究[J].计算机应用研究, 2014, 31(9):2696-2710. XIONG Haijun, ZHU Yongli, ZHAO Jianli, et al. Research on Protocol Modeling Method Based on Behavior Trees and Its Application[J]. Application Research of Computers, 2014, 31(9):2696-2710.
[23] 解方,段富.从行为树转换到UML状态机来验证系统需求[J].计算机工程与设计,2013,34(10):3710-3716. XIE Fang, DUAN Fu. Validation of System Requirements from Behavior Tree to UML State Machine[J]. Computer Engineering and Design, 2013, 34(10):3710-3716.
[24] UMEDA Y, ISHII M, YOSHIOKA M, et al. Supporting Conceptual Design Based on the Function-behavior-state Modeler[J]. Artificial Intelligence for Engineering Design, Analysis and Manufacturing, 1996, 10(4):275-288.
[25] KWIATKOWSKA M, NORMAN G, PARKER D.PRISM 4.0:Verification of Probabilistic Real-time Systems[C]//Proceedings of the 23rd International Conference on Computer Aided Verification. Snowbird, UT:Springer, 2011:585-591.
[26] 侯翌,杨培林,徐凯,等. 基于概率模型检测的机电系统动态可靠性评价[J].中国机械工程, 2019, 30(5):549-553. HOU Yi, YANG Peilin, XU Kai, et al. Dynamic Reliability Evaluation Approach for Electromechanical Systems Based on Probabilistic Model Checking[J].China Mechanical Engineering, 2019, 30(5):549-553.
[27] 姜潮,李文学,王彬,等. 一种针对概率与非概率混合结构可靠性的敏感性分析方法[J].中国机械工程, 2013, 24(19):2577-2583. JIANG Chao,LI Wenxue,WANG Bin,et al.A Structural Reliability Sensitivity Analysis Method for Hybrid Uncertain Model with Probability and Non-probabilistic Variables[J]. China Mechanical Engineering, 2013, 24(19):2577-2583.