概率行為樹模型轉化為模型檢測模型方法研究

侯 翌，楊培林，徐 凱

（西安交通大學機械工程學院，陜西 西安 710049）

1 引言

由于機電系統(tǒng)的功能與結構日趨復雜，其可靠性問題日顯突出，可靠性已成為衡量機電系統(tǒng)性能的重要指標之一。

為了提高機電系統(tǒng)可靠性分析特別是FMEA 分析的準確性與效率，近年來有學者對基于模型檢測的機電系統(tǒng)可靠性評價進行了研究[1-6]?；谀Ｐ蜋z測對機電系統(tǒng)進行可靠性評價時首先要建立系統(tǒng)的形式化模型，然后借助模型檢測工具（Model Checker）自動遍歷系統(tǒng)的形式化模型（形式化驗證）進而實現(xiàn)可靠性評價，因此能有效提高可靠性分析特別是FMEA 分析的準確性與效率。用模型檢測工具提供的建模語言進行形式化建模難度較大，為了使機電系統(tǒng)的形式化建模過程更加直觀并降低建模難度，通常采用圖形化的建模方法進行形式化建模，然后再將其轉化為模型檢測工具所能接受的形式化模型（模型檢測形式化模型，即利用模型檢測工具提供的建模語言建立的模型），以便于后續(xù)的形式化驗證和可靠性評價。

概率行為樹PBT（Probabilistic Behavior trees）作為一種圖形化建模方法[7-13]，具有嚴格的形式化語義和圖形句法，其建模思路接近系統(tǒng)的需求模型和設計模型，具有良好的層次特性并易于維護，因此特別適合復雜機電系統(tǒng)的形式化建模。以利用概率模型檢測工具PRISM[14]（Probabilistic Symbolic Model Checker）對機電系統(tǒng)進行可靠性評價為背景，首先對機電系統(tǒng)的概率行為樹建模進行了介紹，分析了概率模型檢測工具PRISM 提供的形式化建模語言，然后定義了從行為樹模型到PRISM形式化模型的轉換規(guī)則，實現(xiàn)了機電系統(tǒng)行為樹模型向模型檢測形式化模型的轉換，為進一步利用概率模型檢測工具PRISM 進行可靠性評價提供了便利。

2 概率行為樹與機電系統(tǒng)的概率行為樹建模

2.1 概率行為樹

概率行為樹 PBT 由節(jié)點（Nodes）和箭頭（Arrows）組成[8]。每個節(jié)點與系統(tǒng)的一個組件（component）相關聯(lián)。節(jié)點的類型包括：狀態(tài)實現(xiàn)節(jié)點、輸入輸出節(jié)點、條件節(jié)點、守衛(wèi)節(jié)點和原子節(jié)點等。箭頭表示控制流，它規(guī)定了節(jié)點信息的傳遞方向。行為樹有三種控制流，分別為：順序流、選擇流和并發(fā)流。較復雜的概率行為樹可由若干子行為樹構成。

行為樹節(jié)點的標簽（Label）指定了控制流的流動方向。帶有標簽的節(jié)點稱為原始節(jié)點，目標節(jié)點指行為樹中與原始節(jié)點有同樣名稱和行為的節(jié)點。不同的標簽具有不同的含義，其中常用的為回溯標簽“^”，如圖1 所示。它表示控制流由原始節(jié)點跳回到目標節(jié)點。

圖1 節(jié)點標簽Fig.1 Node Label

2.2 機電系統(tǒng)的概率行為樹建模

基于概率行為樹的語義和特征，可用概率行為樹描述機電系統(tǒng)的行為過程，實現(xiàn)對機電系統(tǒng)的概率行為樹建模。機電系統(tǒng)概率行為樹模型中的節(jié)點主要包括以下幾種。

2.2.1 狀態(tài)實現(xiàn)節(jié)點

狀態(tài)實現(xiàn)節(jié)點表達了機電系統(tǒng)功能載體變遷過程中所處的某種狀態(tài)。例如某傳感器處于高電平狀態(tài)，則可用節(jié)點表示，如圖2 所示。

圖2 狀態(tài)實現(xiàn)節(jié)點Fig.2 State Realization Node

2.2.2 輸入輸出節(jié)點

輸入輸出節(jié)點表達各功能載體發(fā)生同步狀態(tài)變遷時的信息交流，如圖3 所示。輸出節(jié)點表示功能載體“電機”發(fā)出信息“電機啟動”；輸入節(jié)點表示功能載體“滾珠絲杠”接受信息“電機啟動”。這時，在信息“電機啟動”驅動下，電機與滾珠絲杠實現(xiàn)同步運動。

圖3 輸出輸入節(jié)點Fig.3 Output and Input Node

2.2.3 守衛(wèi)節(jié)點

守衛(wèi)節(jié)點描述機電系統(tǒng)功能載體發(fā)生變遷的使能條件（事件）。守衛(wèi)節(jié)點中的概率信息λ 表示該守衛(wèi)節(jié)點前后狀態(tài)實現(xiàn)節(jié)點之間的狀態(tài)變遷率。例如某傳感器從“正?！睜顟B(tài)向“失效”狀態(tài)變遷時，其對應的守衛(wèi)節(jié)點，如圖4 所示。圖中：λ—傳感器的失效率。

圖4 守衛(wèi)節(jié)點Fig.4 Guard Node

2.2.4 原子節(jié)點

原子節(jié)點用于表示機電系統(tǒng)功能載體的多狀態(tài)并發(fā)，原子節(jié)點中的狀態(tài)實現(xiàn)節(jié)點之間用短豎線（|）連接。例如電機在滿足“啟動電機”這一變遷條件時，同時發(fā)出“啟動運行”的信號，這兩個行為可用原子節(jié)點表示，如圖5 所示。

圖5 原子節(jié)點Fig.5 Atomic Node

3 模型檢測工具PRISM 及其形式化建模語言

概率模型檢測工具PRISM 一種廣泛使用的概率模型檢測工具，它支持多種概率模型，如連續(xù)時間馬爾科夫鏈CTMC（Continuous Time Markov Chains）、馬爾科夫決策 MDP（Markov Decision Processes）、概率時間自動機 PTA（Probabilistic Timed Automata）等，適用于復雜系統(tǒng)的概率模型檢驗[13]。

PRISM 建模語言由模塊（Modules）和變量（Variables）兩種基本元素組成。PRISM 形式化模型由一個或多個模塊構成，各模塊之間可以交互作用。模塊由變量和命令組成，如圖6 所示。圖中：x—模塊的變量，“［］x=0->0.6：（x′=1）”—模塊中的命令。

圖6 PRISM 模塊Fig.6 PRISM Module

變量可以是局部變量（屬于特定模塊）也可以是全局變量（屬于整個模型）。一個模塊包含一個或多個局部變量，這些變量的值組成了模塊的狀態(tài)。比如電機有“關閉”和“啟動”兩個狀態(tài)，PRISM 建模語言會將電機狀態(tài)描述為：motor：［0..1］

其中motor 為變量，motor=0 代表電機處于關閉狀態(tài)，motor=1 代表電機處于啟動狀態(tài)。

模塊的行為（狀態(tài)的變遷）通過命令（commands）來定義，命令由守衛(wèi)（guard）和更新（update）組成，命令的組成形式為：

［］guard->prob_1：update_1+…prob_n：update_n

其中，守衛(wèi)描述的是狀態(tài)變遷執(zhí)行需要滿足的條件，即“事件”。守衛(wèi)由模型的變量值（可以是該模塊中的局部變量也可以是其他模塊中的變量）描述，更新描述了變遷后的狀態(tài)。當滿足守衛(wèi)時便可以執(zhí)行相應的變遷，變遷的概率由prob_i 表示。當系統(tǒng)模型為CTMC 時，prob_i 表示的是狀態(tài)變遷率。比如傳感器有“正?！焙汀笆А眱蓚€狀態(tài)，PRISM 語言描述為 sensor：［0..1］，0 代表“正?！?，1 代表“失效”，則：［］sensor=0->λ：（sensor′=1）

表示傳感器從正常狀態(tài)向失效狀態(tài)的變遷，狀態(tài)變遷率為λ。

如果系統(tǒng)中兩個或多個變遷同步發(fā)生，可以通過同步（synchronization）的方式實現(xiàn)對該種情況的描述，具體而言就是在命令前的方括號內(nèi)加入同樣的“標記”。此時，加入“標記”的命令同時執(zhí)行，即發(fā)生同步變遷。

按照PRISM 語言規(guī)則，同步變遷率為參與同步變遷的各個變遷率的乘積。實際建模時，通常將一條同步變遷語句中的變遷率直接設定為同步變遷率，而把其他同步變遷語句中的變遷率設定為1。例如，電機（Motor）通過滾珠絲杠帶動工作臺（workbench）運動，電機正轉時工作臺前進，電機反轉時工作臺后退。當電機由正轉變?yōu)榉崔D，工作臺則由前進變?yōu)楹笸恕６叩淖冞w可以看作是同時發(fā)生的。描述該過程的PRISM 模型，如圖7 所示。二者通過在命令前的方括號內(nèi)加入標記“return”實現(xiàn)了變遷的同步，同步狀態(tài)變遷率為Lambda。

圖7 同步變遷Fig.7 Synchronization Transition

4 概率行為樹模型到PRISM 模型的轉換

4.1 轉換規(guī)則

通過研究概率行為樹與PRISM 建模語言的語義和句法，根據(jù)行為樹模型與PRISM 形式化模型相關元素之間的對應關系，得到概率行為樹模型與PRISM 形式化模型之間的轉換規(guī)則如下。

轉換規(guī)則1：行為樹模型中功能載體名稱轉換為PRISM 模型中模塊的名稱和變量名，行為樹模型中每個子行為樹對應PRISM 模型中的一個模塊。行為樹模型中電機子行為樹轉換為PRISM 模型中的電機（Motor）模塊，如圖8 所示。工作臺（Workbench）子行為樹轉換為PRISM 模型中的工作臺模塊。

圖8 功能載體名稱的轉換Fig.8 Conversion of Functional Carrier Name

轉換規(guī)則2：行為樹模型中任意子行為樹的狀態(tài)實現(xiàn)節(jié)點數(shù)對應PRISM 模型中該模塊的狀態(tài)數(shù)，按照狀態(tài)實現(xiàn)節(jié)點的出現(xiàn)順序從（0～n）自動排序，且初始狀態(tài)始終為“0”。其中，回溯節(jié)點與其目標節(jié)點為同一節(jié)點，不再參與排序。在出現(xiàn)并發(fā)流的情況下，分支從左到右依次排序。電機（Motor）子行為樹共有三個狀態(tài)實現(xiàn)節(jié)點，則PRISM 模型中電機模塊則有三個狀態(tài)，其中0 代表正轉“forward”、1 代表反轉“reverse”、2 代表關機“stop”，初始狀態(tài)為“0”，如圖9 所示。

圖9 狀態(tài)實現(xiàn)節(jié)點的轉換Fig.9 Conversion of State Realisation Node

轉換規(guī)則3：行為樹模型中兩狀態(tài)實現(xiàn)節(jié)點間的守衛(wèi)節(jié)點轉換為PRISM 模型中與之對應兩狀態(tài)間的變遷條件（守衛(wèi)），守衛(wèi)節(jié)點中的概率信息轉換為狀態(tài)變遷率，如圖10 所示。

圖10 守衛(wèi)節(jié)點的轉換Fig.10 Conversion of Guard Node

轉換規(guī)則4：行為樹模型中輸入輸出節(jié)點的信息轉換為PRISM 模型中同步變遷命令語句前的同步標志。圖中分別為工作臺（Workbench）和傳感器（Sensor）子行為樹，傳感器安裝在工作臺的前端（front），如圖11 所示。當工作臺離開前端時，便會發(fā)出信息“l(fā)eave”，傳感器收到此信息后由高電平狀態(tài)（high）向低電平狀態(tài)（low）變遷。輸入輸出節(jié)點中的信息“l(fā)eave”轉換為相應變遷語句前面的同步標志，表示兩個狀態(tài)變遷同步進行。

轉換規(guī)則5：行為樹模型中子行為樹之間有信息通訊時（通過輸入輸出節(jié)點實現(xiàn)），PRISM 模型各模塊間的同步變遷語句中只有輸出節(jié)點對應的變遷語句具有變遷率，其余輸入節(jié)點對應的變遷語句中的變遷率缺?。ㄔ赑RISM 語句中變遷率缺省時默認為1）；子行為樹之間無信息通訊時，PRISM 模型中變遷語句的變遷率則不能缺省。由于工作臺子行為樹中是輸出節(jié)點，傳感器子行為樹中是輸入節(jié)點，故PRISM 模型中只有工作臺模塊的同步變遷語句中有“1/60”的變遷率，傳感器的同步變遷語句中的變遷率自動缺省，如圖11 所示。

圖11 輸入輸出節(jié)點的轉換Fig.11 Conversion of Input and Output Node

4.2 建模工具開發(fā)

基于上述轉換規(guī)則，利用C#開發(fā)了機電系統(tǒng)概率行為樹建模工具 BTEditor（Behavior Trees Editor），如圖12 所示。利用該建模工具不僅可以創(chuàng)建機電系統(tǒng)的概率行為樹模型，還可以將該行為樹模型自動轉換為PRISM 代碼（PRISM 形式化模型），為下一步利用模型檢測工具PRISM 進行可靠性評估提供了方便。

圖12 行為樹建模工具BTEditorFig.12 Behavioral Tree Modeling Tools BTEditor

5 實例分析

以簡化后的機床工作臺系統(tǒng)為例。在該系統(tǒng)中，共有三個功能載體，分別是電機（Motor）、工作臺（Workbench）和上極限位置傳感器（Topsenor）。電機帶動工作臺在上極限位置和下極限位置間做往復運動。當電機正轉時，工作臺由上極限位置向下極限位置運動；當電機反轉時，工作臺由下極限位置向上極限位置運動。在工作臺的上極限位置設有上極限位置傳感器，當工作臺到達上極限時，上極限位置傳感器由低電平變?yōu)楦唠娖剑姍C則會改變旋轉方向；反之，當工作臺離開上極限時，上極限位置傳感器會由高電平變?yōu)榈碗娖?。工作臺到達下極限位置時電機會自動改變旋轉方向（實際上在下極限位置也設有極限位置傳感器，為簡化起見在此略去）。根據(jù)各功能載體的行為邏輯，分別建立了三個功能載體的子行為樹，如圖13 所示。

圖14 數(shù)控機床工作臺系統(tǒng)PRISM 模型Fig.14 PRISM Model of Workbench System of CNC Machine Tool

根據(jù)上述轉換規(guī)則，將行為樹模型轉換為PRISM 形式化模型，如圖14 所示。電機、上極限位置傳感器與工作臺三個功能載體分別對應PRISM 模型中的三個模塊。各模塊分別描述了三功能載體在上極限傳感器正常和故障兩種狀態(tài)時的狀態(tài)變遷。

6 結論

建立機電系統(tǒng)的形式化模型是利用概率模型檢測工具對其進行可靠性評價的前提。根據(jù)機電系統(tǒng)概率行為樹模型與PRISM 建模語言的語義和句法，給出了由概率行為樹模型向模型檢測工具PRISM 形式化模型轉換的規(guī)則。利用轉換規(guī)則，可直接從機電系統(tǒng)的概率行為樹模型轉換為模型檢測形式化模型，避免了直接使用模型檢測語言建模帶來的困難，為基于概率模型檢測的機電系統(tǒng)可靠性評價提供了方便。