侯 翌 楊培林 徐 凱 劉 青 樊娟妮

1.西安交通大學(xué)機(jī)械工程學(xué)院，西安，7100492.西北工業(yè)集團(tuán)有限公司計(jì)量理化一中心，西安，710043

0 引言

隨著機(jī)電一體化技術(shù)的發(fā)展，機(jī)電系統(tǒng)的集成度和復(fù)雜程度越來越高，不僅機(jī)電系統(tǒng)的性能會(huì)隨時(shí)間發(fā)生變化，而且系統(tǒng)組成單元之間往往具有復(fù)雜的耦合關(guān)系，因此機(jī)電系統(tǒng)的動(dòng)態(tài)可靠性越來越引起人們的關(guān)注。

目前對系統(tǒng)動(dòng)態(tài)可靠性進(jìn)行分析評(píng)價(jià)的主要方法有狀態(tài)空間法、動(dòng)態(tài)故障樹分析(dynamic fault tree analysis，DFTA)法、Petri網(wǎng)等[1-2]。狀態(tài)空間法以馬爾可夫(Markov)模型為基礎(chǔ)，通過求解狀態(tài)轉(zhuǎn)移方程計(jì)算系統(tǒng)可靠性指標(biāo)，但當(dāng)系統(tǒng)規(guī)模較大時(shí)，直接應(yīng)用馬爾可夫過程理論建立系統(tǒng)的可靠性模型比較困難[3]。DFTA在傳統(tǒng)故障樹分析(fault tree analysis，F(xiàn)TA)的基礎(chǔ)上增加了一些用于描述動(dòng)態(tài)特性的邏輯門，如功能相關(guān)門、順序強(qiáng)制門、優(yōu)先與門等，在一定程度上加強(qiáng)了其動(dòng)態(tài)描述性能，并通過轉(zhuǎn)化為馬爾可夫模型或動(dòng)態(tài)貝葉斯網(wǎng)絡(luò)得到了定量結(jié)果[4-6]，但當(dāng)系統(tǒng)較復(fù)雜時(shí)，動(dòng)態(tài)故障樹建模困難。Petri方法具有圖形化建模和定量數(shù)學(xué)計(jì)算的優(yōu)點(diǎn)，可以利用馬爾可夫過程理論或蒙特卡羅(Monte Carlo)仿真計(jì)算可靠性指標(biāo)，但系統(tǒng)較復(fù)雜時(shí)，也會(huì)增加Petri網(wǎng)的建模難度[7]。

模型檢測是一種形式化的自動(dòng)驗(yàn)證技術(shù)，用于檢驗(yàn)有限狀態(tài)系統(tǒng)是否滿足某種給定性質(zhì)[8-11]。概率模型檢測是對模型檢測的拓展，它不僅能夠驗(yàn)證系統(tǒng)性質(zhì)的正確性，還能夠自動(dòng)計(jì)算系統(tǒng)性質(zhì)出現(xiàn)的概率[12-13]。本文對概率模型檢測進(jìn)行了介紹并將其引入機(jī)電系統(tǒng)的動(dòng)態(tài)可靠性評(píng)價(jià)中，通過對機(jī)電系統(tǒng)可靠性問題的形式化建模、可靠性指標(biāo)的形式化規(guī)約，利用概率模型檢測工具自動(dòng)計(jì)算可靠性指標(biāo)，實(shí)現(xiàn)基于概率模型檢測的機(jī)電系統(tǒng)動(dòng)態(tài)可靠性評(píng)價(jià)。

1 模型檢測及概率模型檢測

模型檢測是一種形式化方法，它首先以某種形式化語言對系統(tǒng)狀態(tài)變遷進(jìn)行描述，即對系統(tǒng)進(jìn)行形式化建模，然后以時(shí)序邏輯公式描述所期望的某種性質(zhì)，即建立性質(zhì)的形式化規(guī)約，最后利用模型檢測工具來搜索系統(tǒng)模型的有窮狀態(tài)空間，自動(dòng)檢驗(yàn)系統(tǒng)是否滿足所期望的性質(zhì)。當(dāng)系統(tǒng)不滿足所期望的性質(zhì)時(shí)，將給出反例說明性質(zhì)為何不成立。

概率模型檢測中的形式化模型是一種隨機(jī)模型，它反映了系統(tǒng)狀態(tài)變遷的隨機(jī)特性。概率模型檢測也需要利用包含概率信息的時(shí)序邏輯語言對所要驗(yàn)證的性質(zhì)進(jìn)行描述，如“系統(tǒng)處于某狀態(tài)的概率小于0.001”等，因此通過概率模型檢測不僅可以判斷某性質(zhì)是否會(huì)發(fā)生，而且能計(jì)算該性質(zhì)發(fā)生的概率。

概率模型檢測可以通過概率模型檢測工具PRISM來進(jìn)行[14]。作為一種廣泛使用的概率模型檢測工具，PRISM支持多種概率模型，如連續(xù)時(shí)間馬爾可夫鏈(continuous time Markov chains，CTMC)、馬爾可夫決策(Markov decision processes，MDP)、概率時(shí)間自動(dòng)機(jī)(probabilistic timed automata，PTA)等。PRISM采用二叉決策圖(binary decision diagram，BDD)和多端二叉決策圖(multi-terminal binary decision diagram，MTBDD)兩種數(shù)據(jù)結(jié)構(gòu)，并融合了圖論計(jì)算和數(shù)值計(jì)算兩類計(jì)算技術(shù)，所以可以構(gòu)建和計(jì)算非常大的系統(tǒng)可達(dá)狀態(tài)空間，并有很高的數(shù)值計(jì)算效率，適用于復(fù)雜系統(tǒng)的概率模型檢驗(yàn)。

2 可靠性指標(biāo)形式化規(guī)約及可靠性評(píng)價(jià)

為了基于概率模型檢測實(shí)現(xiàn)機(jī)電系統(tǒng)的動(dòng)態(tài)可靠性評(píng)估，本文利用PRISM提供的形式化建模語言建立機(jī)電系統(tǒng)的形式化模型，用連續(xù)隨機(jī)邏輯(continuous stochastic logics，CSL)對機(jī)電系統(tǒng)的可靠性指標(biāo)進(jìn)行形式化規(guī)約。

2.1 機(jī)電系統(tǒng)的形式化建模

概率模型檢測工具PRISM提供的形式化建模語言包括模塊(modules)和變量(variables)兩種基本元素[14]。模型由一個(gè)或多個(gè)模塊構(gòu)成，一個(gè)模塊包含一個(gè)或多個(gè)變量，變量用來描述狀態(tài)。模塊的定義形式為

module name

?

endmodule

模塊的行為通過命令(commands)來定義，命令由守衛(wèi)(guard)和更新(update)組成，命令的形式為

[] guard ->prob：update

一條命令反映了一次狀態(tài)變遷過程，其中g(shù)uard描述的是狀態(tài)變遷需要滿足的條件，當(dāng)條件滿足時(shí)便可進(jìn)行狀態(tài)的變遷(更新)。update為變遷(更新)后的狀態(tài)，狀態(tài)變遷過程的狀態(tài)轉(zhuǎn)移率由prob表達(dá)。命令前面的方括號(hào)[]中可添加執(zhí)行標(biāo)記，標(biāo)記相同的命令是同步執(zhí)行的。

對機(jī)電系統(tǒng)進(jìn)行形式化建模時(shí)，每個(gè)組成單元用一個(gè)模塊來描述，各個(gè)模塊組成整個(gè)系統(tǒng)的形式化模型。模塊中的命令反映了單元狀態(tài)的變遷條件、變遷后的狀態(tài)及狀態(tài)轉(zhuǎn)移率等信息。對于動(dòng)態(tài)可靠性中的相關(guān)失效問題，單元失效之間的關(guān)聯(lián)性可在變遷條件中進(jìn)行描述。

2.2 可靠性指標(biāo)的形式化規(guī)約及可靠性評(píng)價(jià)

PRISM支持多種形式化規(guī)約語言，對基于CTMC的系統(tǒng)形式化模型，PRISM用連續(xù)隨機(jī)邏輯CSL來描述所期望的性質(zhì)。由于系統(tǒng)的狀態(tài)變遷過程都對應(yīng)一條狀態(tài)路徑，因此CSL定義了狀態(tài)公式和路徑公式，分別用于描述系統(tǒng)所處的狀態(tài)及狀態(tài)在路徑上的時(shí)序關(guān)系。

狀態(tài)公式的巴科斯范式為

-φ∷true|a|φ∧φ| ┐φ|S～c[φ]|P～c[ψ]

(1)

其中，a表示每個(gè)原子公式都是狀態(tài)公式；符號(hào)∧和┐分別表示邏輯與和邏輯非；“～”表示運(yùn)算符，～ ∈{<， >， ≤， ≥}，S～c[φ]表示狀態(tài)φ成立的概率滿足比較運(yùn)算符指定的約束c，P～c[ψ]表示路徑ψ成立的概率滿足比較運(yùn)算符指定的約束c。

路徑公式的巴科斯范式為

-ψ∷=XIφ|φ1UIφ2

(2)

其中，“X”和“U”為時(shí)態(tài)算子，分別表示“下一步”和 “直到”，XIφ描述了從當(dāng)前狀態(tài)下經(jīng)過時(shí)間段I進(jìn)入狀態(tài)φ；φ1UIφ2表示在時(shí)間段I內(nèi)，狀態(tài)φ1一直成立直到狀態(tài)φ2成立。

PRISM對CSL進(jìn)行了擴(kuò)展，在路徑公式中添加了時(shí)態(tài)算子“G”(表示全局)和“F”(表示將來某時(shí)刻)，同時(shí)引入操作符“P=？”和“S=？”分別用于描述一個(gè)路徑公式成立的概率以及一個(gè)狀態(tài)的穩(wěn)態(tài)概率。另外PRISM對邏輯運(yùn)算符作了重新定義，如用“&”表示“∧”，用“<=”表示“≤”等。

對機(jī)電系統(tǒng)進(jìn)行可靠性評(píng)價(jià)時(shí)，對所關(guān)注的系統(tǒng)狀態(tài)用上述狀態(tài)公式進(jìn)行規(guī)約，并用路徑公式規(guī)約相應(yīng)的可靠性指標(biāo)。例如若關(guān)注某系統(tǒng)“單元R處于狀態(tài)r并且單元Q處于狀態(tài)q”這一狀態(tài)在時(shí)間t內(nèi)出現(xiàn)的概率，則針對這一評(píng)價(jià)指標(biāo)建立的CSL規(guī)約表達(dá)式為

P=?[F=tR=r&Q=q]

(3)

式(3)表示時(shí)間t內(nèi)“單元R處于狀態(tài)r并且單元Q處于狀態(tài)q”的概率是多少。

將上述機(jī)電系統(tǒng)的形式化模型及可靠性指標(biāo)的CSL規(guī)約表達(dá)式輸入概率模型檢測工具PRISM，即可針對CSL規(guī)約表達(dá)式進(jìn)行模型檢驗(yàn)并能自動(dòng)求解表達(dá)式成立的概率，從而實(shí)現(xiàn)可靠性評(píng)價(jià)。

3 實(shí)例分析

圖1 主軸箱驅(qū)動(dòng)系統(tǒng)原理Fig.1 Principle of spindle box drive system

圖1為某五軸聯(lián)動(dòng)數(shù)控機(jī)床主軸箱的驅(qū)動(dòng)系統(tǒng)示意圖。系統(tǒng)通過安裝平衡油缸來平衡主軸箱的自重，從而減輕電機(jī)、絲杠和軸承等部件的負(fù)載。當(dāng)平衡油缸正常工作時(shí)，由于平衡油缸的平衡作用，滾珠絲杠及軸承所受負(fù)載較小。當(dāng)平衡油缸系統(tǒng)由于某種原因造成油液泄漏而使油缸支撐失效時(shí)，絲杠和軸承2(推力軸承)會(huì)承受比油缸正常工作時(shí)更大的負(fù)載(軸承1為向心軸承，忽略油缸對其影響)，其壽命也會(huì)隨之下降，即由于平衡油缸的失效會(huì)加劇其他部件的失效，因此該系統(tǒng)的失效為相關(guān)失效。

設(shè)所有部件的壽命服從指數(shù)分布，平衡油缸的失效率為8(10-6h-1)，其他部件的失效率如表1所示。

表1 各部件的失效率

上述主軸箱驅(qū)動(dòng)系統(tǒng)的正常工作條件是滾珠絲杠、軸承1及軸承2正常工作，平衡油缸的作用只是減緩系統(tǒng)的失效。按照前文提到的方法，可以建立系統(tǒng)的形式化模型，如圖2所示。其中平衡油缸對軸承2和滾珠絲杠失效的影響體現(xiàn)在相應(yīng)的狀態(tài)變遷條件中，見圖2b和圖2d所示的模型。

(a)平衡油缸模型

(b)滾珠絲杠模型

(c)軸承1模型

(d)軸承2模型圖2 主軸箱驅(qū)動(dòng)系統(tǒng)形式化模型Fig.2 Formal model of spindle box drive system

依據(jù)主軸箱驅(qū)動(dòng)系統(tǒng)的正常工作條件，可建立如下的可靠性評(píng)價(jià)指標(biāo)形式化規(guī)約：

P=?[F=tba=0&b1=0&b2=0]

(4)

式(4)表示主軸箱驅(qū)動(dòng)系統(tǒng)在時(shí)間t內(nèi)正常工作的概率，即可靠度。依據(jù)上述形式化模型及可靠性指標(biāo)形式化規(guī)約，通過PRISM進(jìn)行模型檢測，可求得系統(tǒng)可靠度，如圖3所示。

圖3 主軸箱驅(qū)動(dòng)系統(tǒng)可靠度Fig.3 Reliability of spindle box drive system

為了驗(yàn)證上述計(jì)算結(jié)果的正確性，本文也用狀態(tài)空間法[15]對此進(jìn)行計(jì)算。該實(shí)例涉及四個(gè)組成單元(平衡油缸、滾珠絲杠、軸承1及軸承2)，考慮每個(gè)單元有正常與失效兩種狀態(tài)，四個(gè)單元組成的系統(tǒng)共有24= 16個(gè)狀態(tài)。根據(jù)狀態(tài)之間的轉(zhuǎn)移率(失效率)可畫出狀態(tài)轉(zhuǎn)移圖并據(jù)此建立16×16階的狀態(tài)轉(zhuǎn)移密度矩陣A(限于篇幅，狀態(tài)轉(zhuǎn)移圖及轉(zhuǎn)移密度矩陣在此不再列出)，由狀態(tài)空間法建立如下的矩陣微分方程：

(5)

P(t)=(p1(t),p2(t),…,p16(t))

其中,P(t)為系統(tǒng)狀態(tài)行向量。

求解該微分方程組，可得系統(tǒng)處于正常狀態(tài)的概率(可靠度)為

(6)

式(6)的計(jì)算結(jié)果與基于PRISM的計(jì)算結(jié)果完全一致，如圖3所示。

在該實(shí)例中，若不考慮失效相關(guān)性，即不計(jì)平衡油缸失效對其他部件失效的影響，則可按傳統(tǒng)方法計(jì)算系統(tǒng)的可靠度。由于滾珠絲杠、軸承1及軸承2在功能上是串聯(lián)關(guān)系，可得到不考慮失效相關(guān)時(shí)的系統(tǒng)可靠度為

R(t)=Rbs·Rb1·Rb2= e-9×10-6t·e-16×10-6t·e-16×10-6t=e-41×10-6t

(7)

式中，Rbs、Rb1、Rb2分別為滾珠絲杠、軸承1和軸承2的可靠度。

主軸箱驅(qū)動(dòng)系統(tǒng)可靠度計(jì)算結(jié)果如圖3所示。可以看出在不考慮失效相關(guān)時(shí)計(jì)算得到的系統(tǒng)可靠度要大于考慮失效相關(guān)時(shí)所得到的可靠度，這會(huì)使可靠性評(píng)價(jià)產(chǎn)生較大的偏差。

4 結(jié)論

(1)利用模型檢測工具提供的形式化建模語言可以描述系統(tǒng)單元的狀態(tài)變遷過程，單元失效之間的關(guān)聯(lián)性可體現(xiàn)在狀態(tài)變遷條件中。

(2)只需分別建立各個(gè)單元的狀態(tài)變遷模型(模塊)，即可構(gòu)建出整個(gè)系統(tǒng)的形式化模型，系統(tǒng)建模過程簡單方便。

(3)通過對可靠性指標(biāo)的形式化規(guī)約，借助模型檢測可自動(dòng)計(jì)算各種可靠性指標(biāo)，提高了可靠性評(píng)價(jià)的效率。