， ，

(南昌航空大學(xué)軟件學(xué)院，南昌 330063)

基于時(shí)間Petri網(wǎng)的綜合航電系統(tǒng)時(shí)序驗(yàn)證分析

樊鑫，鄭巍，梁旗軍

(南昌航空大學(xué)軟件學(xué)院，南昌330063)

綜合航電系統(tǒng)是一種對(duì)可靠性、實(shí)時(shí)性要求非常高的嵌入式應(yīng)用系統(tǒng);為了解決針對(duì)復(fù)雜應(yīng)用場(chǎng)景下綜合航電系統(tǒng)的處理時(shí)間和工作時(shí)序預(yù)估較困難、且計(jì)算自動(dòng)化程度不高等測(cè)試驗(yàn)證問(wèn)題，提出了一種基于時(shí)間約束Petri網(wǎng)的綜合航電系統(tǒng)時(shí)序驗(yàn)證和分析方法;給出了時(shí)間約束Petri網(wǎng)的形式化定義，分析了綜合航電系統(tǒng)工作流程中各節(jié)點(diǎn)的時(shí)間屬性，通過(guò)引入時(shí)序約束路徑的概念，并提出了時(shí)序推理算法;通過(guò)在仿真算例中進(jìn)行計(jì)算并對(duì)比實(shí)際運(yùn)行數(shù)據(jù)，結(jié)果表明該方法在針對(duì)綜合航電系統(tǒng)運(yùn)行時(shí)序的驗(yàn)證分析方面具有有效性。

綜合航電系統(tǒng)；時(shí)間Petri網(wǎng)；時(shí)序約束路徑；時(shí)序推理算法

0 引言

綜合模塊化航空電子(integrated modular avionics，IMA)是目前航空電子系統(tǒng)體系結(jié)構(gòu)發(fā)展的最新階段，在國(guó)內(nèi)通常被稱為綜合航電系統(tǒng)。由于綜合航電系統(tǒng)具有系統(tǒng)綜合化且較之一般應(yīng)用軟件，絕大多數(shù)綜合航電軟件對(duì)實(shí)時(shí)性要求更高，需要能及時(shí)、正確響應(yīng)外部發(fā)生的隨機(jī)事件。這些特征給綜合模塊化航電系統(tǒng)的測(cè)試和驗(yàn)證帶來(lái)了新的問(wèn)題和挑戰(zhàn)。國(guó)內(nèi)外學(xué)者近年來(lái)開(kāi)展了大量的研究，在仿真測(cè)試環(huán)境搭建[1-2]、模型驅(qū)動(dòng)的測(cè)試驗(yàn)證方法[3-4]及系統(tǒng)建模[5]等方面均提出了相應(yīng)的方法。文獻(xiàn)[2]提出一種分布式仿真測(cè)試環(huán)境的軟件體系結(jié)構(gòu)設(shè)計(jì)，該結(jié)構(gòu)應(yīng)用代理模式，解決了分布式測(cè)試環(huán)境節(jié)點(diǎn)間實(shí)時(shí)通訊的關(guān)鍵技術(shù)，且該測(cè)試平臺(tái)已成功地應(yīng)用于多個(gè)航電軟件的系統(tǒng)測(cè)試中。文獻(xiàn)[3]和文獻(xiàn)[4]分別選擇SysML順序圖和活動(dòng)圖模型對(duì)航電嵌入式軟件進(jìn)行系統(tǒng)建模，并提出了集成測(cè)試和安全性測(cè)試方法。綜合以上的研究工作，目前針對(duì)綜合航電系統(tǒng)時(shí)間特性的驗(yàn)證方法研究較少，且UML或SysML模型本身在時(shí)間屬性的表述能力方面相對(duì)欠缺，因此，如何能對(duì)綜合航電系統(tǒng)的時(shí)間屬性進(jìn)行驗(yàn)證和分析是目前需要研究的重要課題。

Petri網(wǎng)能夠?qū)﹄x散并行系統(tǒng)進(jìn)行嚴(yán)密的數(shù)學(xué)表示，且物理意義清楚、推理過(guò)程簡(jiǎn)潔、易于自動(dòng)化，在近年來(lái)受到越來(lái)越多的關(guān)注。為了使Petri網(wǎng)能夠更好地描述系統(tǒng)的時(shí)間屬性和系統(tǒng)可調(diào)度性，國(guó)內(nèi)不少學(xué)者已經(jīng)完成了很多前期的基礎(chǔ)性研究，并擴(kuò)展了Petri網(wǎng)模型的時(shí)間信息表達(dá)能力[6]，且在電力系統(tǒng)故障的預(yù)測(cè)和診斷領(lǐng)域得到了廣泛地應(yīng)用和實(shí)踐[7-9]。文獻(xiàn)[6]提出了時(shí)間Petri網(wǎng)的混合語(yǔ)義模型，并提出了狀態(tài)類分析方法，用以模型的可調(diào)度性分析和時(shí)間計(jì)算。文獻(xiàn)[7]利用電力系統(tǒng)故障過(guò)程中，警報(bào)信息中蘊(yùn)含的時(shí)間信息，提出了一種時(shí)間溯因推理的電網(wǎng)智能診斷報(bào)警方法。文獻(xiàn)[8]通過(guò)充分分析電網(wǎng)警報(bào)信息的時(shí)序?qū)傩院捅Ｗo(hù)斷路器動(dòng)作的邏輯規(guī)則，提出了一種基于時(shí)間約束Petri網(wǎng)的電網(wǎng)警報(bào)處理及故障診斷方法。文獻(xiàn)[9]針對(duì)診斷模型容錯(cuò)性不強(qiáng)的問(wèn)題，提出了一種融合時(shí)序約束網(wǎng)絡(luò)的模型Petri網(wǎng)故障診斷模型。

在綜合航電系統(tǒng)的運(yùn)行過(guò)程中，各子系統(tǒng)或各分區(qū)應(yīng)用系統(tǒng)的處理活動(dòng)也具有相應(yīng)的時(shí)間屬性。尤其在復(fù)雜應(yīng)用場(chǎng)景下，由于子系統(tǒng)和各分區(qū)應(yīng)用系統(tǒng)的數(shù)據(jù)交互增多且并發(fā)、轉(zhuǎn)移活動(dòng)也相應(yīng)增加，給手工分析驗(yàn)證時(shí)間屬性帶來(lái)了較大困難。因此，分析綜合航電系統(tǒng)中各交互活動(dòng)的時(shí)間屬性，并引入時(shí)間Petri網(wǎng)來(lái)對(duì)系統(tǒng)進(jìn)行建模和仿真，對(duì)研究綜合航電系統(tǒng)時(shí)間屬性的驗(yàn)證方法具有重要的意義。

本文分析了綜合航電系統(tǒng)中各交互活動(dòng)的時(shí)序?qū)傩?，并研究了存在的時(shí)間約束關(guān)系，通過(guò)引入時(shí)間Petri網(wǎng)(Timed Petri Net)，提出了一種基于時(shí)序約束路徑的時(shí)序推理算法，該方法能夠有效地計(jì)算綜合航電系統(tǒng)工作流程中各節(jié)點(diǎn)的時(shí)間屬性，為系統(tǒng)驗(yàn)證分析提供了有效的解決方法。

1 時(shí)間Petri網(wǎng)

1.1 時(shí)間約束定義

時(shí)間約束是為更好地描述時(shí)間屬性而定義的用于約束相應(yīng)時(shí)間屬性的范圍信息，主要包含時(shí)間點(diǎn)約束和時(shí)間段約束。

1)時(shí)間點(diǎn)約束。

時(shí)間點(diǎn)約束定義為時(shí)間區(qū)間T(t)=[t,t+]，用以描述事件發(fā)生時(shí)間t的不確定性，即事件發(fā)生的確切時(shí)間t屬于約束范圍T(t)，t∈T(t)。

2)時(shí)間長(zhǎng)度約束。

時(shí)間長(zhǎng)度是兩個(gè)時(shí)間點(diǎn)之間的時(shí)間跨度。用δ(ti,tj)表示時(shí)間點(diǎn)ti和tj之間的時(shí)間跨度，即δ(ti,tj)=tj-ti。時(shí)間長(zhǎng)度約束定義為Δ(ti,tj) =[Δtij,Δtij+],表示時(shí)間長(zhǎng)度δ(ti,tj)的約束范圍，即δ(ti,tj)∈Δ(ti,tj)，且Δtij和Δtij+分別表示時(shí)間段δ(ti,tj)的最小取值和最大取值。

1.2 TPN形式化描述

根據(jù)Petri網(wǎng)的定義，并考慮事件的時(shí)序?qū)傩?，將TPN定義為六元組：

TPN= {P,T,I,O,F,δ}

其中：P={p1,p2,…,pn}，為庫(kù)所的有限集合；T={t1,t2,…,tn}，為變遷的有限集合；I：T→P為從變遷到所有庫(kù)所得輸入映射函數(shù)；O：T→P為從變遷到所有庫(kù)所得輸出映射函數(shù)；F?(T×P) ∪(P×T)為庫(kù)所和變遷之間所有關(guān)聯(lián)弧的集合；δ={δ1,δ2,…,δn}為對(duì)應(yīng)所有變遷的時(shí)間約束條件集合。

圖1 一個(gè)簡(jiǎn)單的TPN

為了方便后續(xù)的討論，假設(shè)pi和tk為T(mén)PN中的某個(gè)庫(kù)所和變遷，則定義tk的最近前驅(qū)庫(kù)所集合NPre(tk)、前驅(qū)庫(kù)所集合Pre(tk)、最近后繼庫(kù)所集合NPost(tk)以及后繼庫(kù)所集合Post(tk)如下：

1)如果存在從庫(kù)所pi到達(dá)變遷tk的弧，則稱pi為變遷tk的前驅(qū)庫(kù)所，變遷tk的所有前驅(qū)庫(kù)所組成的集合即為變遷tk的前驅(qū)庫(kù)所集合，記為集合Pre(tk)，將變遷tk最近的前驅(qū)庫(kù)所構(gòu)成的集合稱為最近前驅(qū)庫(kù)所集合NPre(tk)；

2)如果存在從變遷tk到達(dá)庫(kù)所pi的弧，則稱pi為變遷tk的后繼庫(kù)所，變遷tk的所有后繼庫(kù)所組成的集合即為變遷tk的后繼庫(kù)所集合，記為集合Post(tk)，將變遷tk最近的后繼庫(kù)所構(gòu)成的集合稱為最近后繼庫(kù)所集合NPost(tk)；

1.3 TPN時(shí)序推理基本規(guī)則

在本文中用Petri網(wǎng)的庫(kù)所表示綜合航電系統(tǒng)中的相應(yīng)活動(dòng)或事件。如果活動(dòng)i的發(fā)生可以觸發(fā)活動(dòng)j的發(fā)生，則活動(dòng)i為活動(dòng)j的前驅(qū)，活動(dòng)j為活動(dòng)i的后繼，可表示為i→j；反之，如果活動(dòng)i發(fā)生了，則活動(dòng)j不發(fā)生，則活動(dòng)i為活動(dòng)j的互斥活動(dòng)，可表示為i?j。假設(shè)庫(kù)所表示的活動(dòng)為i,j,k,p,q在時(shí)間點(diǎn)ti,tj,tk,tp,tq發(fā)生，且活動(dòng)關(guān)系為p→q，q→i，i→j，j→k。

1)前向時(shí)序推理規(guī)則

前向時(shí)序推理可推導(dǎo)出后繼活動(dòng)的時(shí)間約束，具體計(jì)算規(guī)則如下：

T(tj)=T(ti) +Δ(ti,tj) = [t+Δtij,t++Δtij+]

(1)

T(tk)=T(ti) +Δ(ti,tj) +Δ(tj,tk) =

[t+Δtij+Δtjk,t++Δtij++Δtjk+]

(2)

2)逆向時(shí)序推理規(guī)則

逆向時(shí)序推理可推導(dǎo)出前驅(qū)活動(dòng)的時(shí)間約束，具體計(jì)算規(guī)則如下：

T(tq)=T(ti)-Δ(tq,ti)=[t-Δtqi,t+-Δtqi+] (3)

T(tp)=T(ti)-Δ(tq,ti)-Δ(tp,tq) =

[t-Δtqi-Δtpq,t+-Δtqi+-Δtpq+]

(4)

2 基于時(shí)間Petri網(wǎng)的綜合航電系統(tǒng)時(shí)序驗(yàn)證算法

2.1 基于時(shí)間Petri網(wǎng)的時(shí)序驗(yàn)證流程

綜合航電系統(tǒng)的時(shí)序驗(yàn)證以綜合航電系統(tǒng)的工作場(chǎng)景為驗(yàn)證對(duì)象，采用時(shí)間Petri網(wǎng)模型對(duì)其進(jìn)行時(shí)序驗(yàn)證主要是用于預(yù)測(cè)在某工作場(chǎng)景下航電系統(tǒng)整體處理時(shí)間的時(shí)間約束和預(yù)期的完成時(shí)間，其驗(yàn)證算法的流程如圖2所示。

圖2 時(shí)間Petri網(wǎng)的時(shí)序驗(yàn)證流程圖

算法中相關(guān)集合的定義如下：

1)活動(dòng)集合A。A={a1,a2,…,an}是航電系統(tǒng)某工作場(chǎng)景中全部活動(dòng)ai的集合。

2)庫(kù)所集合P。P={p1,p2,…,pn}是將航電系統(tǒng)某工作場(chǎng)景轉(zhuǎn)換為T(mén)PN模型后的庫(kù)所集合，在轉(zhuǎn)換時(shí)工作場(chǎng)景中的活動(dòng)ai可對(duì)應(yīng)庫(kù)所pi。

3)變遷集合T。T={t1,t2,…,tn}為將航電系統(tǒng)某工作場(chǎng)景轉(zhuǎn)換為T(mén)PN模型后的變遷集合。變遷ti的定義如下：

?a1<.a2|a1,a2∈A→?ti|ti×p2∈I∧p1×ti∈O

其中，a1<.a2表示活動(dòng)a2在活動(dòng)a1執(zhí)行后立即執(zhí)行，且活動(dòng)a1，a2在TPN中對(duì)應(yīng)的庫(kù)所為p1，p2。

4)路徑集合L。L={l1,l2,…,ln}為在TPN中從原因庫(kù)所到結(jié)束庫(kù)所的庫(kù)所序列組成的路徑集合，li=。

2.2 基于時(shí)間Petri網(wǎng)的時(shí)間長(zhǎng)度推理算法

基于時(shí)間Petri網(wǎng)的時(shí)間長(zhǎng)度推理算法(TPN Time Distance Reasoning Algorithm， 簡(jiǎn)稱TDRA算法)，是根據(jù)執(zhí)行路徑上的各庫(kù)所的時(shí)間長(zhǎng)度約束信息來(lái)推理最終執(zhí)行完的時(shí)間長(zhǎng)度約束的計(jì)算算法，其計(jì)算公式和方法如下：

1)假設(shè)計(jì)算路徑為li=，即從pi開(kāi)始到pm結(jié)束。

2)如果li=不存在并發(fā)活動(dòng)所產(chǎn)生的庫(kù)所，且遷移關(guān)系也沒(méi)有并發(fā)關(guān)系，則計(jì)算方式為：

TL i= ∑{Δ(ti,tj),Δ(tj,tk), ...,Δ(tm’,tm) }

=Δ( ∑{Δtij,Δtjk,...Δtm’m},

∑{Δtij+,Δtjk+,...Δtm’m+})

(5)

3)如果li=存在并發(fā)活動(dòng)所產(chǎn)生的庫(kù)所，且遷移關(guān)系為并發(fā)關(guān)系，則計(jì)算方式為：

TL i=max{Δ(ti,tj),Δ(tj,tk), ...,Δ(tm’,tm) }

=Δ(max{Δtij,Δtjk,...Δtm’m},

max{Δtij+,Δtjk+,...Δtm’m+})

(6)

2.3 基于時(shí)間Petri網(wǎng)的時(shí)間點(diǎn)推理算法

基于時(shí)間Petri網(wǎng)的時(shí)間點(diǎn)推理算法(TPN Time Spot Reasoning Algorithm， 簡(jiǎn)稱TSRA算法)，是根據(jù)執(zhí)行路徑上的各庫(kù)所的時(shí)間長(zhǎng)度約束信息來(lái)推理最終執(zhí)行完的預(yù)估時(shí)間的計(jì)算算法，其計(jì)算公式和方法如下：

1)假設(shè)計(jì)算路徑為li=，即從pi開(kāi)始到pm結(jié)束。

2)在時(shí)間點(diǎn)推理算法中，需要為每個(gè)庫(kù)所表示的事件或動(dòng)作設(shè)置一個(gè)時(shí)間段占比參數(shù)drij，drij表示在δ(ti,tj)時(shí)間長(zhǎng)度內(nèi)pi通常會(huì)以何種比例的時(shí)間完成所對(duì)應(yīng)的事件或動(dòng)作，drij的取值可通過(guò)實(shí)際測(cè)試運(yùn)行而統(tǒng)計(jì)得到。例如：若事件pi的時(shí)間長(zhǎng)度約束為[20 ms,40 ms]，且其時(shí)段占比drij=50%，則可計(jì)算出實(shí)際所需的時(shí)間為20 + (40-20) ×50% =30 ms。

3)如果li=不存在并發(fā)活動(dòng)所產(chǎn)生的庫(kù)所，且遷移關(guān)系也沒(méi)有并發(fā)關(guān)系，則計(jì)算方式為：

TL i=

∑{δ(ti,tj) ×drij,δ(tj,tk) ×drjk, ...,δ(tm’,tm) ×drm’m} =

δ(ti,tj) ×drij+δ(tj,tk) ×drjk+ ... +δ(tm’,tm) ×drm’m

(7)

4)如果li=都是并發(fā)活動(dòng)所產(chǎn)生的庫(kù)所，且遷移關(guān)系為并發(fā)關(guān)系，則計(jì)算方式為：

TL i=

max{δ(ti,tj) ×drij,δ(tj,tk) ×drjk, ...,δ(tm’,tm) ×drm’m}

(8)

2.4 算法的實(shí)現(xiàn)

TSRA算法和TDRA算法是以深度遍歷優(yōu)先算法為基礎(chǔ)，對(duì)TPN遍歷從而產(chǎn)生計(jì)算路徑并以此計(jì)算相應(yīng)時(shí)間屬性。TSRA算法如下。

Algorithm1TimeSpotReasonAlgoInput：TPNOutput：estimatedtimeTSET(TPN)1)Path(TPN)=Depth＿traverse(TPN)2)Foreachpathli：;pi，pj，…pm>inSetPath(TPN)3){sett0asthebeginningtimeofli4)setpi=getPlace(li)5)While(piisnotNULL)6){setcurDur=δ(ti，tj)?drij7)If(isPlaceParellel(pi)==true)8){setp’i=getNextPlace(li)9)setcurDur’=δ’(ti，tj)?dr’ij10)If(curDur;curDur’)11)setcurDur=curDur’12)}setsumDur=sumDur+curDur13)setpi=getNextPlace(li)14)}15)settLi=t0+sumDur16)addtLitoTSET(TPN)17)}

3 仿真算例系統(tǒng)驗(yàn)證與分析

本文選擇了某綜合模塊化航電系統(tǒng)在綜合導(dǎo)航場(chǎng)景下的系統(tǒng)處理過(guò)程來(lái)建立TPN模型，如圖3所示。TPN模型描述了在綜合導(dǎo)航場(chǎng)景下以裝載飛行計(jì)劃、獲取當(dāng)前位置、計(jì)算飛行位置、修正IRS累計(jì)誤差以及調(diào)整飛機(jī)姿態(tài)等庫(kù)所表示的處理動(dòng)作的發(fā)生流程、順序以及每個(gè)庫(kù)所之間的遷移情況，且模型中庫(kù)所的描述信息如表1所示。

圖3 綜合航電系統(tǒng)綜合導(dǎo)航場(chǎng)景的TPN模型

1)在綜合導(dǎo)航場(chǎng)景的TPN模型中，P3和P4庫(kù)所表示的是并發(fā)發(fā)生的動(dòng)作，則推理時(shí)間點(diǎn)和時(shí)間長(zhǎng)度約束屬性時(shí)應(yīng)采用(6)式和(8)式進(jìn)行計(jì)算。

表1 某航電系統(tǒng)綜合導(dǎo)航TPN的庫(kù)所列表

2)通過(guò)綜合航電系統(tǒng)的實(shí)際測(cè)試和統(tǒng)計(jì)，將庫(kù)所p1～p11的時(shí)間段占比參數(shù)drij均設(shè)為60%。

從綜合導(dǎo)航場(chǎng)景TPN模型中生成了3條執(zhí)行路徑，并采用TSRA算法和TDRA算法分別計(jì)算出了針對(duì)每條執(zhí)行路徑的預(yù)計(jì)完成時(shí)間和時(shí)間長(zhǎng)度約束，如表2所示。

表2 綜合航電系統(tǒng)綜合導(dǎo)航場(chǎng)景的時(shí)間驗(yàn)證

從表2所列舉的預(yù)期與實(shí)際時(shí)間可以比較得出，最小的偏差為9 ms，最大的偏差為11 ms，相對(duì)于預(yù)計(jì)時(shí)間的偏差比例最小為3.5%，最大為4.3%，但均不超過(guò)5%。

為了進(jìn)一步對(duì)本文所提出的方法進(jìn)行驗(yàn)證，另外選取了航電系統(tǒng)地形跟隨、起飛后數(shù)據(jù)檢查、降落后數(shù)據(jù)檢查及機(jī)電系統(tǒng)收起落架等5個(gè)場(chǎng)景進(jìn)行TPN建模與時(shí)間推理計(jì)算，5個(gè)場(chǎng)景共驗(yàn)證并計(jì)算了66條執(zhí)行路徑的預(yù)計(jì)時(shí)間，并分析了平均偏差比例。

表3 其他應(yīng)用實(shí)例中的驗(yàn)證情況

綜合表2和表3可以看出，在多個(gè)實(shí)例系統(tǒng)的測(cè)試驗(yàn)證過(guò)程中，文中所提出的基于時(shí)間Petri網(wǎng)的時(shí)間推理算法，能夠?qū)ο到y(tǒng)的時(shí)間屬性較準(zhǔn)確地分析和估計(jì)，平均偏差比例不小于5%。

4 結(jié)論

本文利用Petri網(wǎng)具有能對(duì)系統(tǒng)進(jìn)行動(dòng)態(tài)描述和分析的特點(diǎn)，通過(guò)擴(kuò)展Petri網(wǎng)的時(shí)間屬性，提出了一種基于時(shí)間Petri網(wǎng)來(lái)分析驗(yàn)證航電系統(tǒng)時(shí)間屬性和時(shí)間約束的方法。從多個(gè)系統(tǒng)的驗(yàn)證結(jié)果分析來(lái)看，該方法能夠有效地對(duì)系統(tǒng)的時(shí)間屬性進(jìn)行建模和計(jì)算，具有較好地可信度，對(duì)航電系統(tǒng)的測(cè)試與驗(yàn)證有積極意義。

[1] 鐘德明, 劉 斌, 阮 鐮. 嵌入式軟件仿真測(cè)試環(huán)境軟件體系結(jié)構(gòu)研究[J]. 北京航空航天大學(xué)學(xué)報(bào). 2005,31(10):1130-1134.

[2]劉 暢, 劉 斌, 阮 鐮. 航空電子軟件仿真測(cè)試環(huán)境軟件體系結(jié)構(gòu)研究[J]. 航空學(xué)報(bào), 2007,27(5):877-882.

[3]鄭 春, 舒 堅(jiān), 牛文生, 等. 基于SysML模塊定義圖的集成測(cè)試序列生成方法[J]. 計(jì)算機(jī)工程與設(shè)計(jì),2016,37(8):2067-2071.

[4]曹偉芳. 基于SysML活動(dòng)圖的測(cè)試序列生成方法研究[D]. 南昌航空大學(xué), 2016.

[5]徐文華, 張育平. 基于航電系統(tǒng)架構(gòu)模型的安全性分析工具的設(shè)計(jì)與實(shí)現(xiàn)[J]. 計(jì)算機(jī)科學(xué),2016,43(11):536-541.

[6]潘 理, 丁志軍, 郭觀七. 混合語(yǔ)義時(shí)間Petri網(wǎng)模型[J]. 軟件學(xué)報(bào),2011,22(6):1199-1209.

[7]楊健維, 何正友, 臧天磊. 基于方向性加權(quán)模糊 Petri網(wǎng)的電網(wǎng)故障診斷方法[J]. 中國(guó)電機(jī)工程學(xué)報(bào), 2010,30(34): 42-49.

[8]楊健維, 何正友. 基于時(shí)序模糊Petri網(wǎng)的電力系統(tǒng)故障診斷[J]. 電力系統(tǒng)自動(dòng)化,2011,35(15):46-51.

[9]張 巖, 張 勇, 文福拴, 等. 容納時(shí)序約束的改進(jìn)模糊Petri網(wǎng)故障診斷模型[J]. 電力系統(tǒng)自動(dòng)化, 2014,38(5):66-72.

TemporalAnalysisofIntegratedAvionicsSystemBasedonTimedPetriNet

Fan Xin，Zheng Wei，Liang Qijun

(School of Software, Nanchang Hangkong University, Nanchang 330063, China)

Integrated avionics system is an embedded application system with high reliability and real time requirement. In order to solve the problem such as estimating and testing processing duration during the verification of integrated avionics system more effectively, an analytical method based on Petri net with time constraints, which is named timed Petri net, is proposed in this paper. The formalized definition of timed Petri net is also introduced after analyzes the time attributes of each working node while integrated avionics system is running. By introducing the concept of temporal constraint path, the temporal reasoning algorithms are designed. At last, comparison and analysis of data collected in the simulation example system are also presented, the results show that the proposed method is feasible and effective in time verification of the integrated avionics system.

Integrated Avionics System; Timed Petri Net; Temporal Constraint Path; Temporal Analysis Algorithm

2017-08-28；

2017-10-11。

國(guó)家自然科學(xué)基金青年基金項(xiàng)目(61501217)。

樊 鑫(1981-)，男，湖北荊州人，講師，主要從事軟件測(cè)試技術(shù)、模型驗(yàn)證技術(shù)方向的研究。

鄭 巍(1982-)，男，江西萍鄉(xiāng)人，副教授，主要從事軟件模型驗(yàn)證、社交網(wǎng)絡(luò)分析方向的研究。

1671-4598(2017)11-0288-03

10.16526/j.cnki.11-4762/tp.2017.11.073

TP391.9

B