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

杨培林1 刘 青2 樊娟妮2 侯 翌1

1. 西安交通大学机械工程学院,西安,710049 2. 西北工业集团有限公司计量理化一中心,西安,710043

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

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

0 引言

机电系统的功能和行为逻辑越来越复杂,系统基本单元的失效往往会使机电系统产生错误的行为逻辑进而导致动作故障(如碰撞、超程等),动作故障不仅影响系统的可靠性运行还可能产生严重的后果。因此在复杂机电系统的设计过程中,针对动作故障对系统可靠性进行全面系统的评价,以尽早发现设计缺陷或可靠性薄弱环节并进行设计改进,就成为复杂机电系统设计过程中的一项重要内容。

传统的系统可靠性评价方法包括可靠性框图(reliability block diagram,RBD)、故障树分析(fault tree analysis,FTA)、失效模式与影响分析(failure modes and effects analysis,FMEA)等[1]。近年来,随着机电系统的日益复杂及对动态可靠性的关注,基于Petri网的可靠性建模与评价方法[2-5]、GO法(GO methodology)[6-7]等得到了广泛应用。这些方法虽然各有所长,但系统故障与单元失效之间的因果、逻辑关系仍依靠领域专家来辨识。为此,有学者对基于模型检测的可靠性评价方法进行了研究[8-12],利用模型检测技术来提高可靠性分析,特别是FMEA分析的自动化水平与准确性。

模型检测是一种验证有限状态系统是否满足某种给定性质的形式化方法,即利用模型检测工具(model checker)遍历系统模型的有穷状态空间,检验系统是否会出现所给定的某种性质[13],概率模型检测还能计算出性质出现的概率。利用概率模型检测技术进行可靠性评价时首先要建立系统的形式化模型,但用模型检测工具提供的形式化建模语言直接对系统进行建模则直观性较差,建模难度大。为此,人们利用图形化的建模方法(如Petri网)对系统建模然后将其转换为模型检测工具能够接受的形式化模型[14-16],避免了直接使用形式化语言进行建模所带来的困难。

Petri网对动态系统有很强的建模能力,已用于模型检测中的形式化建模,但由于Petri网建模缺乏层次性,系统较大时建模困难且难维护。概率行为树(probabilistic behavior trees,PBT)是一种基于状态变迁的图形化建模方法[17-23],建模思路接近系统的需求模型和设计模型,可以采用逐步构建的方式进行层次化建模(首先建立各个单元的子行为树,然后集成为系统的行为树),并且概率行为树模型易于转换为形式化建模语言(如PRISM)[19-20]

本文首先分析机电系统功能执行过程中的状态及其变迁,对基于概率行为树的机电系统形式化建模进行研究并开发了相应的支持工具;以机电系统运行过程中潜在的动作故障发生概率为评价指标,基于机电系统的概率行为树模型,通过概率模型检测实现了对机电系统的可靠性评价。

1 机电系统功能执行过程中的状态及其变迁

1.1 机电系统的功能执行过程

机电系统通常包括驱动子系统、执行子系统、信息处理及控制子系统和传感检测子系统。根据机电系统的功能层次结构(总功能-子功能-元功能),机电系统的各个子系统可以进一步分解,直至约定层次的功能载体。

依据机电系统的功能-行为-状态(function-behavior-state,FBS)映射关系[24],功能通过功能载体的行为来实现,而行为可表达为功能载体的状态及其变迁,因此机电系统的功能执行过程就可看作为系统功能载体的状态迁移过程,是一种离散事件动态系统。

1.2 机电系统中功能载体的状态

机电系统中功能载体的状态S取决于功能载体的行为,S= f(P), f : PS,其中P为功能载体的行为特征空间。机电系统中的功能载体可以分为4类:机械执行构件类功能载体、驱动类功能载体、控制类功能载体、测试传感类功能载体。根据功能载体的功能和行为,本文将功能载体行为过程中的特征状态概括为以下几种。

(1)位置状态。位置状态是反映功能载体特征位置的状态,如机电系统执行构件运动过程中的某些特定位置或位姿等。

(2)静动状态。静动状态是反映功能载体是否运动的状态,例如机电系统中的原动机开启或关闭时,将驱动或终止系统工作,因此原动机的运动情况通常可以用开启或关闭这两种状态表示。

(3)物理状态。以物理状态变化为特征的功能载体,可用相关的物理量来表达其状态,如压力、温度及检测传感装置中的高、低电平信号等。

1.3 机电系统中功能载体状态的变迁

将机电系统状态变迁的使能条件称为事件。在机电系统状态变迁这一离散事件动态系统中,事件驱动状态变迁,而变迁后的状态又可能导致新事件的产生。状态变迁可用三元组表示为ST={SET},其中S为状态集合,E为事件集合,T为状态之间变迁有向弧的集合。例如,直线导轨控制系统发出启动电机指令是事件,直线电机在这一事件驱动下由静止状态变迁为移动状态。变迁后直线电机的移动状态又会产生新的事件启动工作台,这一事件驱动与之相连的工作台由静止状态变迁为移动状态。

机电系统中有些功能载体的状态变迁具有同步性,驱动同步状态变迁的事件称为同步事件。如上述直线电机的状态变迁与工作台的状态变迁可认为是同步发生的,驱动其同步状态变迁的同步事件可以认为是启动运行。

若计及功能载体的失效,状态变迁模型中还需要表达单元从正常状态向失效状态的变迁。例如正常情况下某传感器有高、低电平两种状态,在考虑失效时还会有某种失效状态,若分别用00、01和1表达这3种状态,则传感器的状态变迁过程如图1所示。这里的失效过程是指与状态无关的失效过程,即从状态00和01同时向状态失效变迁。若不关注高、低电平状态,可从功能性故障角度将传感器状态分为正常和失效两种状态,即把00、01合并为0(正常状态),原状态变迁简化为正常状态0至失效状态1的变迁。

图1 传感器状态变迁
Fig.1 State transitions of the sensor

1.4 状态转移率

在机电系统的整个生命周期内,从统计学意义上讲,机电系统的状态变迁具有随机特性,包括正常的状态变迁和正常状态与失效状态之间的变迁。

正常变迁时,由于工作环境、工作对象的不确定,机电系统的状态变迁会表现出随机性(不确定性)。例如,由于工件的不同,数控机床会有不同的工艺动作、进给速度和工作行程等。因此在整个生命周期内,可以认为机电系统的状态变迁时间服从指数分布规律,并可用状态变迁时间δ(数学期望)的倒数表示状态转移率λ,即

λ=1/δ

(1)

机电系统从正常状态向失效状态变迁时,系统单元的失效时间通常服从指数分布规律,因此可用单元的失效率表示状态转移率。

2 概率行为树

概率行为树(PBT)由行为树扩展而来[19-20,23]。行为树由节点(nodes)和箭头(arrows)组成。每个节点与系统的一个组件(component)相关联,箭头表示控制流,它规定了节点信息的传递方向。

行为树节点有多种类型,与本文相关的主要节点类型包括:

(1)状态实现节点。状态实现节点表示系统组件处于某种状态,这种状态可以是组件自身状态,也可以是其他组件状态在该组件中的反映。例如,传感器处于高电平时,控制器相应通道获得传感器高电平信号,这时可通过传感器的状态来间接表达控制器的状态,如图2所示。

图2 状态实现节点
Fig.2 State realization node

(2)输入输出节点。输入输出节点描述系统各组件之间的信息通信,如图3a和图3b所示,前者为输入节点,表示组件接收信息(该信息驱动状态变迁);后者为输出节点,表示组件发送信息。

(a) 输入节点

(b) 输出节点

图3 输入输出节点
Fig.3 Input node and output node

(3)条件节点与守卫节点。条件节点中的状态(行为)满足时,控制流通过该节点,否则控制流终止;守卫节点中,若状态(行为)不满足,则一直等待直至满足为止。如图4所示。

(a) 条件节点

(b) 守卫节点

图4 条件节点与守卫节点
Fig.4 Condition node and guard node

(4)原子节点。原子节点内的各节点状态或行为(如输入输出节点的信息通信)同时产生,不会被其他节点的行为所打断。图5所示为原子节点的两种表示形式,其中,图5a描述同一组件的系列状态同时发生;图5b描述不同组件的状态同时发生。

(a) 同一组件

(b) 不同组件

图5 原子节点
Fig.5 Atom node

行为树的控制流有顺序流、选择流和并发流3种。其中顺序流表示一连串状态实现节点通过箭头顺序实现;选择流表示条件分支,控制流沿着满足条件的分支流动;并发流表示控制流沿着所有分支并行流动。

在行为树的状态实现节点上,可以通过标签(label)来指明下一步控制流的方向。其中常采用回溯(reversion)标签“”(图6)表明控制流由原始节点(带有标签的节点)跳回到目标节点(与原始节点有同样组件名称和行为的父节点)。

图6 行为树节点标签
Fig.6 Node label of behavior trees

为了表达系统的随机行为,可以在上述行为树的基础上对其进行概率扩展,形成概率行为树。在概率行为树中,守卫节点增添概率信息λ,表示状态变迁时的状态转移率,如图7所示。

图7 概率行为树输入节点
Fig.7 Input node of PBT

3 机电系统的概率行为树建模

3.1 概率行为树建模

基于机电系统的状态变迁及行为树的语义和句法,可利用概率行为树对机电系统的状态变迁过程进行形式化描述,建立机电系统状态变迁过程的形式化模型,具体方法如下。

机电系统状态变迁过程中的状态用行为树的状态实现节点表达。多状态并发时利用行为树的原子节点来表达,状态变迁过程中的使能条件(事件)用行为树的守卫节点来表达,变迁时的状态转移率用守卫节点中的概率信息来表示。在机电系统的概率行为树模型中,守卫节点不仅表示事件对状态变迁的驱动,还包含了变迁时的状态转移率。

驱动同步状态变迁的同步事件用行为树的输入输出节点来表达。输出节点表示产生同步事件,输入节点表示接受同步事件。输入输出节点与表示状态变迁的守卫节点形成原子节点,表示同步事件与状态变迁是同步发生的。

图8用概率行为树描述了前述直线电机的状态变迁过程,变迁过程中产生了同步事件启动运行和停止运行。

图8 直线电机状态变迁的行为树模型
Fig.8 Behavior trees model of state transitions
for linear motor

利用以上方法可以对机电系统各单元的状态变迁过程进行形式化描述。借助行为树中的输入输出节点(事件)可将各单元的状态变迁模型联系起来,形成机电系统的可靠性概率行为树(probabilistic behavior tree for reliability,PBTR)模型。PBTR会因考虑不同单元的失效而有不同的形式,例如考虑系统单元i和单元j失效时系统概率行为树模型可用PBTRij表示。

3.2 支持工具开发

为了支持可靠性建模,开发了基于概率行为树的可靠性建模支持工具BTEditor (图9)。该软件不仅可以对行为树进行编辑,建立机电系统行为树模型,还可以从行为树模型自动生成概率模型检测工具PRISM所能接受的PRISM语言代码(反应式模块形式语言)[25],为利用模型检测进行可靠性评估提供了便利。

图9 行为树建模工具BTEditor
Fig.9 Behavior tree modeling tool BTEditor

4 基于概率行为树模型的可靠性评价

利用建模支持工具BTEditor建立机电系统的概率行为树模型并将其转换为用PRISM代码表示的形式化模型后,进一步确定可靠性评价中需要关注的系统潜在故障,然后依据潜在故障建立可靠性评价指标,并对其形式化规约。形式化规约后的可靠性评价指标就是模型检测中待验证的系统性质。基于以上的形式化模型及可靠性评价指标的形式化规约就可以通过模型检测器PRISM对机电系统进行可靠性评价[24],如图10所示。

图10 基于概率行为树模型的可靠性评估
Fig.10 Reliability evaluation based on PBT

进行可靠性评价时,应结合具体的评价内容,选用相应的概率行为树模型[26-27]。例如若要评价系统中单元i和单元j失效时对系统可靠性的影响,则应采用概率行为树模型PBTRij进行模型检测。

系统潜在故障用系统单元状态的组合来表达。基于潜在故障的可靠性评价指标用PRISM中的连续随机逻辑(continuous stochastic logics,CSL)[19]进行规约[25]

例如,若“单元A处于状态p且单元B状态处于q”将会导致碰撞,则依据这一潜在故障建立可靠性评价指标,其CSL规约表达式为

P=?[F <= t A=p & B=q]

(2)

式(2)表示t个时间单位内“单元A处于状态p且单元B状态处于状态q”(即产生碰撞)的概率。

5 实例分析

以某数控机床工作台系统为例,说明其行为树建模及可靠性评价过程。机床工作台系统包括工作台、伺服电机、上极限开关和下极限开关(由于行为树模型的描述会占用较大空间,限于篇幅本文忽略系统中的其他单元,如丝杠机构等)。系统运行时,若工作台运行至上下极限开关处,极限开关将由低电平变为高电平,伺服电机反向运转,否则工作台超程。

工作台在上下极限位置之间运动时,系统中的上极限开关(Topsensor)和下极限开关(Bottomsensor)在低电平状态和高电平状态之间迁移。该实例中考虑极限开关总是低电平这一失效模式,并设失效率为λs。若把极限开关的低电平状态和高电平状态合并为正常(normal)状态,则针对上极限开关由正常状态到失效(failure)状态变迁的概率行为树模型如图11所示。类似可得下极限开关的概率行为树模型,不再赘述。

图 11 上极限开关的概率行为树模型
Fig.11 PBT model of top sensor

工作台系统正常运行时,伺服电机(Motor)在正转(fwd)与反转(rev)两种状态之间变迁(状态转移率为λw)。当电机变为正转时产生事件forward,这时工作台由上向下运动;反转时产生事件reverse,工作台由下向上运动。当极限开关失效时(Topsensor=failure或Bottomsensor=failure),电机按原方向转动,不会反向转动,同时产生两个事件bs-fail和ts-fail,分别表示伺服电机继续正转与反转,其概率行为树模型如图12所示。

图12 伺服电机概率行为树模型
Fig.12 PBT model of servo motor

极限开关正常时,工作台(Workbench)在事件forward和reverse驱动下,在上极限(toplimit)和下极限(bottomlimit)两种状态之间变迁。极限开关失效后,工作台在两个事件bs-fail和ts-fail驱动下进行状态变迁。其概率行为树模型如图13所示。

图 13 工作台概率行为树模型
Fig.13 PBT model of workbench

该实例关注的潜在故障如下:①工作台移动到上极限位置时伺服电机继续运行(上超程);②工作台移动到下极限位置时伺服电机继续运行(下超程)。

对于以上两种潜在故障,利用CSL可建立如下的可靠性评价指标。

评价指标1: P=?[ F<=t Workbench=toplimit & Motor=rev](时间t内上超程出现的概率,即上超程故障率,用F1表示)。

评价指标2: P=?[ F<=t Workbench=bottomlimit & Motor=fwd](时间t内下超程出现的概率,即下超程故障率,用F2表示)。

评价指标3: P=?[ F<=t (Workbench=toplimit & Motor=rev)| Workbench=bottomlimit & Motor=fwd] (时间t内上超程或下超程出现的概率,即超程故障率,用F表示)。

设工作台的状态转移率λw为0.016 min-1,极限开关的失效率λs为6×10-8 min-1。利用支持工具BTEditor将上述概率行为树模型转换为PRISM代码,并根据3个评价指标利用PRISM进行模型检测。结果表明:极限开关失效情况下,工作台系统将会产生超程故障。这是因为极限开关失效时,始终保持低电平,不能变迁为高电平,也就不能使伺服电机反向运转,从而导致超程。各种超程故障率随时间的变化如图14a、图14b、图14c所示。若以不超程作为系统的可靠性指标,则工作台系统可靠度为R=1-F,其随时间变化的曲线见图14d。

(a) 上超程故障率F1

(b)下超程故障率F2

(c) 超程故障率F

(d) 系统可靠度R

图 14 工作台系统故障率及可靠度
Fig.14 Fault rate and reliability of workbench system

由以上实例的分析过程可知,概率行为树是一种图形化建模方法,用其对机电系统状态变迁过程进行建模直观方便,将概率行为树模型转换为PRISM代码并建立可靠性评价指标的形式化规约后,即可借助模型检测工具进行可靠性指标的自动计算,提高了可靠性分析的效率与自动化水平。

6 结论

(1)给出了基于概率行为树的机电系统形式化建模方法,基于概率行为树模型并借助模型检测实现了对机电系统的可靠性评价。

(2)概率行为树可以对机电系统状态变迁过程中的状态、事件、状态转移率等进行形式化描述。利用守卫节点可以表达状态变迁过程中的使能条件;利用输入节点与输出节点中的同步事件可以表达同步的状态变迁过程。

(3)机电系统概率行为树建模可以采用逐步构建的方式进行,即可以先建立系统单元的概率行为树模型,然后借助行为树中的状态、输入输出节点(事件)将各单元的状态变迁模型联系起来,形成机电系统的概率行为树模型。

(4)基于概率行为树的机电系统形式化建模比直接使用形式化语言建模直观、易于理解和掌握。利用建模支持工具BTEditor将概率行为树模型转换成PRISM代码并对可靠性评价指标进行形式化规约,通过模型检测器PRISM可实现对机电系统的可靠性评价。

参考文献

[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 2010 8th 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.

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

YANG Peilin1 LIU Qing2 FAN Juanni2 HOU Yi1

1. School of Mechanical Engineering, Xi’an JiaoTong University, Xi’an, 710049 2. No.1 Center of Measuring and Physical-Chemical Performance Testing, Northwestern Industrial Group Co., Ltd., Xi’an, 710043

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

开放科学(资源服务)标识码(OSID):

中图分类号:TH122

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

收稿日期:2019-06-05

基金项目:国家自然科学基金资助项目(51375365)

(编辑 王旻玥)

作者简介:杨培林,男,1963年生,教授。研究方向为机电系统可靠性与动力学、机器人等。E-mail: plyang@mail.xjtu.edu.cn。