盧楠, 王曉東, 唐政, 何佩
1.西北工業大學寧波研究院, 浙江 寧波 315103;2.西北工業大學 計算機學院, 陜西 西安 710072;3.中國電子科技集團公司數據鏈技術重點實驗室, 陜西 西安 710072
隨著新一代人工智能技術和自主技術快速走向戰場,將催生新型作戰力量,顛覆傳統戰爭模式,未來戰爭必將是智能化戰爭。無人機集群作戰作為智能作戰的重要形式,正在嶄露頭角。采用建模仿真方法對無人機集群作戰的有關問題開展研究,可為這一新型作戰樣式的發展和運用提供理論支撐,具有重要現實意義。文獻[1]提出了一種擴展混成Petri網模型并對無人駕駛車輛系統的躲避障礙場景進行建模。文獻[2]提出一種混成Petri網作為信號控制交叉口市區交通網絡的模型。文獻[3]提出了一種基于AOP的時空Petri網的CPS模型,并以智能機器人為例,將該模型成功應用到其故障檢測和修復中。文獻[4]提出了一種混成時空Petri網的CPS實時事件模型,并以醫療控制系統為例,分析了其建模方法的可靠性。
然而,當前針對無人機的建模多以單一物理實體為研究對象進行建模,缺少結合異構無人機集群特點,深度融合離散狀態和連續過程、物理和計算過程的建模與實戰應用場景建模形式化驗證的研究。為此,面向集群建模技術在集群作戰仿真中的迫切需求,從作戰任務需求出發,研究基于時空混成Petri網的異構無人機集群機動行為模型構建方法,定義交互事件解決一體化建模問題。最后選取UPPALL工具對所建模型進行驗證。
無人機飛行過程中的狀態變化量可以表示為[5]
u=[xg,yg,zg,θ,φ,ψ,p,q,r,V,α,β,m]T
式中,依次為3個方位參數、俯仰角、滾轉角、偏航角、滾轉角速度、俯仰角速度、偏航角速度、速度矢量(又分為三軸速度分量u,v,w)、迎角、側滑角和質量。
無人系統集群可以看作一個包括物理空間和信息空間的典型賽博物理系統。在無人機執行任務中,信息物理系統之間的交互可以看作感知和控制事件之間的交互,感知事件包括速度、高度、俯仰角、翻滾角等關鍵屬性信息的感知,控制事件包括各種機動動作,如平飛加減速、俯沖、躍升和戰斗轉彎等。
1) 感知事件模型定義
定義傳感器感知無人機關鍵屬性這一事件為元感知事件,該事件是否發生僅由一個關鍵屬性的數值大小決定。定義元感知事件的形式化模型為:
定義1元感知事件形式化模型
es:τ〈x,c〉
式中:es為某一類元感知事件;τ為該類事件名稱;x為相關屬性名稱;c為觸發條件;f為函數,f:x→R;x為函數中任一變量。
定義2感知事件觸發規則
式中:OP為屬性值數量關系操作符號;D為某一實數;c為感知事件觸發規則。如無人機平飛加減速機動動作,Acc〈a,a>0〉用Acc表示機動動作名稱,a為關鍵屬性,當a的值大于0時,事件平飛加速Acc觸發,無人機隨即開始執行平飛加速機動動作。又因為無人機任務執行過程是包含時空屬性的,故將在某一時刻某一空間地點的某感知事件模型表示為Acc〈a,a=30,l0〉@t0,l0和t0分別代表感知交互事件的時間和空間屬性。
無人機大多機動動作的觸發是由多個關鍵屬性和多個元感知事件共同控制。在定義1的基礎上,X重新定義為組合感知事件相關的屬性名稱,C為感知事件觸發的條件集合。在定義2的基礎上,將組合感知事件模型定義為:
定義3組合感知事件模型定義
2) 交互事件模型定義
無人機的每個機動行為都是以事件為驅動產生的,定義交互事件模型為:
定義4定義交互事件為四元組:
Ei=(es,Capture,Reactor,ec)
4個參數分別為交互事件中的感知事件、感知事件的接收者、感知事件的響應者或者控制事件的產生者、交互事件中的控制事件,其中控制事件又可以定義為
ec:=τ〈Y,N〉
式中:Y為包含多個關鍵屬性的集合;N為關鍵屬性具體值的集合。
異構無人機集群系統是既有離散行為也有連續行為的混成系統。對混成系統建模方法有形式化和非形式化兩種,由于非形式化方法無法窮盡地檢測系統所有可能的狀態,故這類方法不具有完備性。在形式化建模方法中有混成自動機、混成行為系統、 混成通信順序進程、混成Petri網等。其中,混成Petri網相比其他方法具有可描述有限狀態、可更精細化描述、應用范圍廣等優勢,故在混成Petri網的基礎上加入時空因素建立時空混成Petri網來描述異構無人機集群系統行為。
定義5時空混成Petri網為一個十元組[6]:
STHP=(P,T,F,W,M0,H,E,V,I,A)
式中:P為有限庫所集合,包含離散行為Pd和隨時間連續變化的Pc,用圓形節點表示;T為有限變遷集合,包含離散行為的Td和隨時間連續變化的Tc,用方形節點表示;F為流關系集合,用有向弧曲表示;W為HPN上的權函數;M0為庫所集合上初始標識向量;H為既包含離散又包含連續的混合函數;E為離散變遷激發結束的條件集合;V為連續變遷的激發速度;I表示時間函數,[t1,t2]表示變遷上的時間區間函數,即事件完成的時間要求;A表示空間位置信息,可以用區域坐標信息或者經緯度表示,Ai=(xi,yi)。
定義6事件和離散變遷是一一對應關系,離散變遷的觸發表明相應事件的發生;
時空混成Petri網中既有離散狀態節點,也有連續狀態節點,通過有向弧來表示它們之間的相互作用,變遷的激發表明有對應事件的發生。
針對異構無人機集群協同作戰,采用基于時間自動機的UPPAAL工具,對建立的模型進行屬性驗證,證明所建模型的可靠性、可達性、有效性和實時性的,以評價建模方法的可行性。
假設由2架偵察無人機、3架攻擊無人機和負責決策的無人機決策控制中心組成異構無人機集群系統,對敵方13架無人機進行偵察攻擊,整個作戰系統如圖1所示。

圖1 異構無人機集群作戰系統場景圖
異構無人機集群系統中物理實體有偵察類無人機實體、打擊類無人機實體和察打一體化無人機實體。將物理實體類分為無人機實體類和傳感器實體類,形式化表示如(1)~(2)式所示
式中:D表示動力學屬性;K表示運動學屬性;S表示偵察行為;A表示攻擊行為;Z表示實體坐標信息;T表示時間點或區間;C1表示傳感數據變化;C2表示傳感數據未變化。
每個類下的物理實體具體定義為:
加速度傳感器:
陀螺儀傳感器
偵察無人機實體
攻擊無人機實體
察打一體無人機實體
式中:STHP表示時空混成Petri網;pf,ph表示直線飛行和定常盤旋機動屬性;pd,pp表示俯沖增速和急上升轉彎機動屬性;Z表示偵察無人機偵察區域、攻擊無人機攻擊區域、決策中心所在區域、偵察無人機監視區域,定義為庫所S1~S6。
在描述整個異構無人機集群作戰任務過程時用庫所表示時空混成Petri網中各個物理實體,用變遷表示物理實體之間信息和控制決策指令的傳輸。
將無人機集群執行任務的整個過程看作是事件順序執行的過程,可將整個過程描述為圖2所示的Petri網。其中,無人機決策控制中心庫所負責發送控制任務。指令發送和信息反饋用變遷T1~T10表示。整個過程每個庫所都有時空屬性,信息獲取和指令發送對應時間點ti,每個庫所中令牌變化時間段對應「t1,t2」。
圖2中各個變遷含義如表1所示。異構無人機集群系統的事件表如表2所示。

圖2 異構無人機集群完成任務Petri網模型

表1 異構無人機集群執行任務過程變遷含義表

表2 異構無人機集群系統事件表
對異構無人機集群打擊任務建模先用Petri網對整體協同打擊過程進行建模,然后用時空混成Petri網對單架打擊無人機機動行為進行建模。
所有打擊無人機到達指定位置后開始打擊任務,3架打擊無人機協同打擊過程可用Petri網描述如圖3所示。

圖3 3架打擊無人機協同打擊過程Petri網表示圖
在圖3中,P0為打擊無人機到達指定打擊區域,Pij表示打擊無人機各自狀態,1≤i≤3,i∈N,1≤j≤3,j∈N。j=1時,無人機開始協同打擊,j=2時,當前序號無人機將自身打擊完成情況發送到控制中心,P4為控制中心接收所有打擊信息。P6為協同打擊任務完成;Tij表示打擊無人機狀態變化。j=1,協同打擊任務下發事件,j=2,開始打擊任務準備完成事件,j=3,當前無人機成功發送打擊任務完成情況到控制中心。T4為控制中心獲取到的信息為沒有完成全部打擊任務,T5為13個打擊目標均已打擊完成。
當用Petri網對3架打擊無人機協同打擊任務整體建模以后,具體單個無人機狀態用時空混成Petri網表示,所建模型如圖4所示。

圖4 單架無人機打擊過程時空混成Petri網表示圖
完成打擊任務先經過平飛加速到達指定打擊空間位置點;再執行俯沖到達第一個目標正上方;然后平飛減速靠近目標;再進行戰斗轉彎;最后快速躍升完成打擊任務。離散庫所表示機動動作的轉移,連續庫所表示打擊無人機運行過程中關鍵屬性數值的變化,連續變遷表示關鍵屬性變化規律。
P1為平飛加速,V從200 m/s加速到300 m/s,在此過程中涉及速度、切向過載等關鍵屬性變化,連續庫所P9表示t1時刻打擊無人機的速度v1,T8表示速度變化的微分方程,即
P10表示t1到ti時刻速度具體變化值ΔV。T1表示平飛加速機動動作完成。P2為俯沖機動動作。T9表示迎角變化的微分方程,即
T2為俯沖機動動作完成。P3表示平飛減速機動動作,與平飛加速機動動作類似。P5表示戰斗轉彎機動動作。T10表示高度變化的微分方程dH=cosθ(vsinφ+vcosφ)-usinθ。T11表示滾轉角變化的微分方程dφ=qcosφ-rsinφ。T4表示戰斗轉彎機動動作完成。P6表示躍升機動動作與俯沖機動動作類似。T5表示躍升機動動作完成。P7表示本次打擊任務完成。T6表示還有待打擊目標需再次到達目標執行打擊任務。T7表示本架無人機已完成所有打擊任務。P8表示打無人機打擊任務結束。
在異構無人機集群打擊實例中,交互事件關鍵屬性包括速度v、高度h、氣流角迎角α、滾轉角φ,X={v,h,α,φ},不同屬性值代表不同事件,對感知事件、控制事件和交互事件建模如下所示:
感知事件模型:
{espeeding(v,v≥200),esubing(α,α≥0),
eturning({h,φ},(h≥2 000)&(φ≥30))}
控制事件模型:
交互事件模型:
2.2 實例模型的形式化驗證
Acc-Action、Sub-Action、Turn-Action、Jump-Action、Attack-Action、Finished-Action6個離散機動動作模塊和Velocity、High、Roll、Pitch4個連續屬性變化模塊,分別表示水平加速機動動作、俯沖機動動作、戰斗轉彎機動動作、躍升機動動作、打擊機動動作和完成任務行為。模塊之間通過同步信道進行交互。將表示離散連續的10個模塊組件分別映射成時間自動機模板,將模塊中執行的每個過程映射為時間自動機模板中的位置,將機動動作轉換事件映射為時間自動將中的同步通道,得到如圖5所示模型。

圖5 實例各個模塊時間自動機模型
時間自動機模型中,圓圈代表系統各種狀態,帶箭頭有向線段代表系統中狀態之間的轉換,紅色圓圈表示當前正在執行的狀態,深藍色數據表示當前狀態的更新操作,綠色數據表示當前狀態的轉移條件,淺藍色數據表示當前狀態的同步信道傳輸。
2.3 實例驗證分析
運用UPPAAL工具[7-8],進行自動分析,得到實例執行打擊任務過程的流程圖,如圖6所示。
基于時間自動機模型,借助UPPAAL工具對無人機打擊過程中的各種屬性進行驗證:
E<>(enemy==13):驗證了完成任務過程中,至少存在一條路徑,最終將13個敵方目標都消滅掉,可驗證模型的可達性;
A<>(Sub.Sub-Completeimplyroll-state==0):驗證了如果俯沖機動動作完成則認為緊接著進入了下一個機動動作——戰斗轉彎,可驗證模型的實時性;

圖6 實例執行打擊任務過程流程圖
E[](h≥0):驗證了過程中的高度屬性不會有負值;
A[](Attack.Attack-Completeimplyenemy==13):驗證了如果打擊任務完成,則敵方13個目標全部被消滅,可驗證模型的有效性;
E<>(Acc.Acc-Complete):驗證了存在水平加速這個機動動作完成這個狀態。
以上驗證的屬性均可代表某一類屬性。驗證結果如圖7所示。

圖7 實例屬性驗證結果
結果表明所建模型能很好地對該實例過程進行描述,性質均驗證通過。該模型滿足可靠性、可達性、有效性和實時性的要求。
針對異構無人機集群作戰仿真中物理實體數字模型描述這一關鍵技術,圍繞異構無人機集群作戰任務過程的建模和驗證,通過對無人機實體和無人機集群關鍵屬性值變化的運動學和動力學方程描述,以及無人機實體的感知事件、控制事件和兩者之間的交互事件的形式化建模,將無人機的建模由單一物理實體增加到多個物理實體;選用時空混成Petri網描述軍用實戰-異構無人機集群打擊過程。該方法有效描述無人機集群系統中物理過程和計算過程的融合過程,刻畫出各節點之間信息的交換和協同。論文采用UPPAAL工具進行驗證和分析,為無人機集群作戰系統提供驗證框架和環境,證明所建模型滿足可靠性、可達性、有效性和實時性要求。