基于時間Petri網的綜合航電系統時序驗證分析

， ，

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

基于時間Petri網的綜合航電系統時序驗證分析

樊鑫，鄭巍，梁旗軍

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

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

綜合航電系統；時間Petri網；時序約束路徑；時序推理算法

0 引言

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

Petri網能夠對離散并行系統進行嚴密的數學表示，且物理意義清楚、推理過程簡潔、易于自動化，在近年來受到越來越多的關注。為了使Petri網能夠更好地描述系統的時間屬性和系統可調度性，國內不少學者已經完成了很多前期的基礎性研究，并擴展了Petri網模型的時間信息表達能力[6]，且在電力系統故障的預測和診斷領域得到了廣泛地應用和實踐[7-9]。文獻[6]提出了時間Petri網的混合語義模型，并提出了狀態類分析方法，用以模型的可調度性分析和時間計算。文獻[7]利用電力系統故障過程中，警報信息中蘊含的時間信息，提出了一種時間溯因推理的電網智能診斷報警方法。文獻[8]通過充分分析電網警報信息的時序屬性和保護斷路器動作的邏輯規則，提出了一種基于時間約束Petri網的電網警報處理及故障診斷方法。文獻[9]針對診斷模型容錯性不強的問題，提出了一種融合時序約束網絡的模型Petri網故障診斷模型。

在綜合航電系統的運行過程中，各子系統或各分區應用系統的處理活動也具有相應的時間屬性。尤其在復雜應用場景下，由于子系統和各分區應用系統的數據交互增多且并發、轉移活動也相應增加，給手工分析驗證時間屬性帶來了較大困難。因此，分析綜合航電系統中各交互活動的時間屬性，并引入時間Petri網來對系統進行建模和仿真，對研究綜合航電系統時間屬性的驗證方法具有重要的意義。

本文分析了綜合航電系統中各交互活動的時序屬性，并研究了存在的時間約束關系，通過引入時間Petri網(Timed Petri Net)，提出了一種基于時序約束路徑的時序推理算法，該方法能夠有效地計算綜合航電系統工作流程中各節點的時間屬性，為系統驗證分析提供了有效的解決方法。

1 時間Petri網

1.1 時間約束定義

時間約束是為更好地描述時間屬性而定義的用于約束相應時間屬性的范圍信息，主要包含時間點約束和時間段約束。

1)時間點約束。

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

2)時間長度約束。

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

1.2 TPN形式化描述

根據Petri網的定義，并考慮事件的時序屬性，將TPN定義為六元組：

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

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

圖1 一個簡單的TPN

為了方便后續的討論，假設pi和tk為TPN中的某個庫所和變遷，則定義tk的最近前驅庫所集合NPre(tk)、前驅庫所集合Pre(tk)、最近后繼庫所集合NPost(tk)以及后繼庫所集合Post(tk)如下：

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

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

1.3 TPN時序推理基本規則

在本文中用Petri網的庫所表示綜合航電系統中的相應活動或事件。如果活動i的發生可以觸發活動j的發生，則活動i為活動j的前驅，活動j為活動i的后繼，可表示為i→j；反之，如果活動i發生了，則活動j不發生，則活動i為活動j的互斥活動，可表示為i?j。假設庫所表示的活動為i,j,k,p,q在時間點ti,tj,tk,tp,tq發生，且活動關系為p→q，q→i，i→j，j→k。

1)前向時序推理規則

前向時序推理可推導出后繼活動的時間約束，具體計算規則如下：

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)逆向時序推理規則

逆向時序推理可推導出前驅活動的時間約束，具體計算規則如下：

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 基于時間Petri網的綜合航電系統時序驗證算法

2.1 基于時間Petri網的時序驗證流程

綜合航電系統的時序驗證以綜合航電系統的工作場景為驗證對象，采用時間Petri網模型對其進行時序驗證主要是用于預測在某工作場景下航電系統整體處理時間的時間約束和預期的完成時間，其驗證算法的流程如圖2所示。

圖2 時間Petri網的時序驗證流程圖

算法中相關集合的定義如下：

1)活動集合A。A={a1,a2,…,an}是航電系統某工作場景中全部活動ai的集合。

2)庫所集合P。P={p1,p2,…,pn}是將航電系統某工作場景轉換為TPN模型后的庫所集合，在轉換時工作場景中的活動ai可對應庫所pi。

3)變遷集合T。T={t1,t2,…,tn}為將航電系統某工作場景轉換為TPN模型后的變遷集合。變遷ti的定義如下：

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

其中，a1<.a2表示活動a2在活動a1執行后立即執行，且活動a1，a2在TPN中對應的庫所為p1，p2。

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

2.2 基于時間Petri網的時間長度推理算法

基于時間Petri網的時間長度推理算法(TPN Time Distance Reasoning Algorithm， 簡稱TDRA算法)，是根據執行路徑上的各庫所的時間長度約束信息來推理最終執行完的時間長度約束的計算算法，其計算公式和方法如下：

1)假設計算路徑為li=，即從pi開始到pm結束。

2)如果li=不存在并發活動所產生的庫所，且遷移關系也沒有并發關系，則計算方式為：

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

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

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

(5)

3)如果li=存在并發活動所產生的庫所，且遷移關系為并發關系，則計算方式為：

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

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

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

(6)

2.3 基于時間Petri網的時間點推理算法

基于時間Petri網的時間點推理算法(TPN Time Spot Reasoning Algorithm， 簡稱TSRA算法)，是根據執行路徑上的各庫所的時間長度約束信息來推理最終執行完的預估時間的計算算法，其計算公式和方法如下：

1)假設計算路徑為li=，即從pi開始到pm結束。

2)在時間點推理算法中，需要為每個庫所表示的事件或動作設置一個時間段占比參數drij，drij表示在δ(ti,tj)時間長度內pi通常會以何種比例的時間完成所對應的事件或動作，drij的取值可通過實際測試運行而統計得到。例如：若事件pi的時間長度約束為[20 ms,40 ms]，且其時段占比drij=50%，則可計算出實際所需的時間為20 + (40-20) ×50% =30 ms。

3)如果li=不存在并發活動所產生的庫所，且遷移關系也沒有并發關系，則計算方式為：

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=都是并發活動所產生的庫所，且遷移關系為并發關系，則計算方式為：

TL i=

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

(8)

2.4 算法的實現

TSRA算法和TDRA算法是以深度遍歷優先算法為基礎，對TPN遍歷從而產生計算路徑并以此計算相應時間屬性。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 仿真算例系統驗證與分析

本文選擇了某綜合模塊化航電系統在綜合導航場景下的系統處理過程來建立TPN模型，如圖3所示。TPN模型描述了在綜合導航場景下以裝載飛行計劃、獲取當前位置、計算飛行位置、修正IRS累計誤差以及調整飛機姿態等庫所表示的處理動作的發生流程、順序以及每個庫所之間的遷移情況，且模型中庫所的描述信息如表1所示。

圖3 綜合航電系統綜合導航場景的TPN模型

1)在綜合導航場景的TPN模型中，P3和P4庫所表示的是并發發生的動作，則推理時間點和時間長度約束屬性時應采用(6)式和(8)式進行計算。

表1 某航電系統綜合導航TPN的庫所列表

2)通過綜合航電系統的實際測試和統計，將庫所p1～p11的時間段占比參數drij均設為60%。

從綜合導航場景TPN模型中生成了3條執行路徑，并采用TSRA算法和TDRA算法分別計算出了針對每條執行路徑的預計完成時間和時間長度約束，如表2所示。

表2 綜合航電系統綜合導航場景的時間驗證

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

為了進一步對本文所提出的方法進行驗證，另外選取了航電系統地形跟隨、起飛后數據檢查、降落后數據檢查及機電系統收起落架等5個場景進行TPN建模與時間推理計算，5個場景共驗證并計算了66條執行路徑的預計時間，并分析了平均偏差比例。

表3 其他應用實例中的驗證情況

綜合表2和表3可以看出，在多個實例系統的測試驗證過程中，文中所提出的基于時間Petri網的時間推理算法，能夠對系統的時間屬性較準確地分析和估計，平均偏差比例不小于5%。

4 結論

本文利用Petri網具有能對系統進行動態描述和分析的特點，通過擴展Petri網的時間屬性，提出了一種基于時間Petri網來分析驗證航電系統時間屬性和時間約束的方法。從多個系統的驗證結果分析來看，該方法能夠有效地對系統的時間屬性進行建模和計算，具有較好地可信度，對航電系統的測試與驗證有積極意義。

[1] 鐘德明, 劉 斌, 阮 鐮. 嵌入式軟件仿真測試環境軟件體系結構研究[J]. 北京航空航天大學學報. 2005,31(10):1130-1134.

[2]劉 暢, 劉 斌, 阮 鐮. 航空電子軟件仿真測試環境軟件體系結構研究[J]. 航空學報, 2007,27(5):877-882.

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

[4]曹偉芳. 基于SysML活動圖的測試序列生成方法研究[D]. 南昌航空大學, 2016.

[5]徐文華, 張育平. 基于航電系統架構模型的安全性分析工具的設計與實現[J]. 計算機科學,2016,43(11):536-541.

[6]潘 理, 丁志軍, 郭觀七. 混合語義時間Petri網模型[J]. 軟件學報,2011,22(6):1199-1209.

[7]楊健維, 何正友, 臧天磊. 基于方向性加權模糊 Petri網的電網故障診斷方法[J]. 中國電機工程學報, 2010,30(34): 42-49.

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

[9]張 巖, 張 勇, 文福拴, 等. 容納時序約束的改進模糊Petri網故障診斷模型[J]. 電力系統自動化, 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。

國家自然科學基金青年基金項目(61501217)。

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

鄭 巍(1982-)，男，江西萍鄉人，副教授，主要從事軟件模型驗證、社交網絡分析方向的研究。

1671-4598(2017)11-0288-03

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

TP391.9

B