陳 聰,洪 中,陳楊楊,張 仕,蔣建民,2
(1. 福建師范大學數學與信息學院,福建 福州 350117;2. 成都信息工程大學軟件工程學院,四川 成都 610103)
涉及對象運動問題的系統被統稱為移動系統,例如智能交通系統、無人機、無人船以及多移動機器人系統[1,2]。保障一個移動系統在運行過程中的安全性是當前研究的一個熱點問題。為解決這一問題,首先應該確保各個移動對象在運動過程中無碰撞,即各移動對象互相隔離。在移動系統中,由于不同移動對象運行速度和到達同一區域的時間存在差異,各個對象將按照一定的序列進出這一共同區域,通過分析該序列即可判斷移動對象之間是否互相隔離。這類序列被稱為調度序列,而對于給定的調度序列,分析其是否能夠確保移動對象之間的互相隔離的過程被稱為可調度性分析。
長期以來,對調度理論[3 - 8]的研究大多集中于任務調度和可調度性分析。前者主要考慮如何生成最優調度策略,后者則主要驗證一個調度中是否存在著違反約束條件的情況。早期提出的實時調度理論側重于研究可調度性條件,如原始的單調速率分析[5]、單調時限調度算法[3]和最早截止時間優先策略[6]。其后續研究[4,7,8]則主要集中在信息物理融合系統CPS(Cyber-Physical System)中調度的優化與實現上[9]。作為任務調度,它們要求被調度的任務之間彼此獨立,互不影響。然而,在移動系統中,由于移動系統與環境區域相互作用,很難將一個移動系統分解成多個獨立的任務,因此使用現有的方法無法直接對移動系統的隔離調度進行建模。
為了解決這個問題,需要一種新的調度理論來描述移動系統[10,11]中各移動對象的移動過程。Jiang等人[11]提出了一種基于事件的調度,其中,事件指的是執行的一個行為或一個簡單的活動。由于一個任務可由多個事件來構成[9],基于事件的調度明顯具有比任務調度更細的粒度。一個復雜的移動系統,雖然很難將其分解成多個獨立的任務,但是卻可以輕易地分解為一系列移動事件。因此,它更適用于移動系統中的調度建模。然而,Jiang等人[11]提出的基于事件的調度并未考慮時間約束,屬于非實時調度,為此,本文在該調度理論的基礎上,加入時間屬性。
要研究移動系統中的實時調度問題,首先必須對移動系統進行建模。現有的主流的實時形式化方法如時間自動機[12,13]、時間進程代數[14 - 16]和時間Petri網[17 - 24]等,都無法方便地對移動系統進行建模。其中,時間自動機無法表示移動系統中多個移動對象的并發行為,而時間進程代數和時間Petri網雖然可以建模并發行為,但卻不能方便地刻畫移動性[11]。鑒于此,本文引入依賴結構DS(Dependency Structure)[11,25]建模移動系統中的移動對象,刻畫其移動性。然而,模型本身并未考慮時間約束,無法建模移動系統的實時性。為此,本文在DS模型的基礎上增加了時間建模能力,擴展出新的模型,稱為時間依賴結構TDS(Time Dependency Structure)。本文將在已有工作[26]的基礎上,從一個典型的智能交通系統入手,進一步完善移動系統的建模方法,同時探討基于事件的實時調度方法,并根據調度序列進行隔離的可調度性分析,以確保移動系統運行過程中的安全性。
計算機體系結構的發展經歷了4個主要階段,即:聯合系統結構、集成的系統結構、系統的體系結構和CPS。為了適應體系結構的變化,調度理論也在不斷發展。傳統的實時調度理論是在相應的可調度性條件下發展起來的,如原始的單調速率分析[5]、單調時限調度算法[3]和最早截止時間優先策略[6]。這類調度理論[3 - 6]大多屬于任務調度。而任務調度理論是在每個調度任務獨立于任何其他任務這一假設前提下進行研究的,換句話說,在目標系統中,嚴格地要求每個被執行的任務之間不會相互影響。
相比傳統的體系結構,CPS的調度更為復雜,因此調度理論的后續研究[4,7,8]主要集中在CPS中調度的優化與實現上[9]。Zhang等人[8]研究了一類受反饋控制規律調節的CPS,探討了這類CPS的任務調度問題,并針對CPS的可預測性能和功耗設計了控制律和任務調度算法;Kim等人[27]將Fork-Join并行任務模型擴展到實時CPS中,使其調度具有實時性,在此基礎上,Kim等人還提出了任務拉伸變換,使得新興的CPS可以從并行實時任務中獲得顯著的好處;Schneider等人[28]研究了由硬實時任務和反饋控制任務組成的混合關鍵度信息物理融合系統MCCPS(Mixed-Criticality Cyber-Physical System)的調度綜合問題,提出了一種MCCPS的多層調度綜合方案,以便在不同的調度層中聯合調度關鍵期限任務和關鍵任務;Liu等人[29]深入分析了車載CPS中時態數據分發的特點,提出了一種基于靜態快照一致性要求的分析請求服務時間范圍的算法,即靜態快照一致性調度算法;Lee等人[30]提出了一種新的周期性容錯CPS任務模型,該模型提高了底層物理子系統的效率和穩定性;de Martini等人[31]提出了適合于CPS的實時調度算法,以便最大限度地提高系統利用率,減少調度開銷,降低上下文切換成本,并對算法進行了仿真;Jiang等人[32]研究了基于多智能體系統的分布式最優調度問題,設計了重新調度算法,以保證CPS系統在擾動情況下的適應性。
從上述工作不難看出,對于調度理論的研究,一般都是先提出調度的度量模型,然后基于該度量模型提出調度算法,最后再對提出的算法進行優化。考慮到現有的研究通常是基于傳統的任務調度,而任務調度要求任務間互相獨立,因而難以處理更細粒度的調度問題。本文提出的基于事件的實時調度可以將一個任務拆分成多個互相聯系的事件,進而對事件進行調度,因此更適用于復雜的移動系統。
建模移動性需要結合界程演算[33,34]。界程演算是發生在封閉且有邊界的界程中的計算,移動對象進入或退出界程均屬于界程演算的范疇。在移動系統中創建界程,需要定位設備與通信技術的支持,以便將系統大環境劃分為許多連續的具有明確邊界的小環境。每個小環境被視為一個界程,使用唯一的標識符表示。在移動系統中,將一個移動對象進入界程定義為進入事件,退出界程定義為退出事件,兩者統稱為移動事件。一般而言,使用進入和退出這兩類移動事件,便可建模一個移動系統的移動性。例如,一個移動對象通過一個界程的過程可以用相繼執行的一個進入事件與一個退出事件來表示。由于復雜的移動系統往往由許多移動對象和界程來組成,系統運行的過程中各個移動對象將不斷地進出不同的界程,從而產生連續的事件序列。

為了幫助讀者理解,圖1給出了一個簡單的智能交通系統的運行示例。該示例描述的是一位乘客John在路口等車并乘車的場景。圖1中的路口區域被劃分成一系列網格,每個網格被視作一個界程,并且進行了編號,將編號為i的界程表示為ci(i=1,2,3,…)。圖1中,車輛A沿著界程c15、c11、c7、c3移動,車輛B沿著界程c8、c7、c6、c5移動,車輛C沿著界程c13、c14、c15、c16移動,John在界程c2中等車,車輛B進入界程c6后John進入車輛B,然后John隨著車輛B繼續向前移動。

Figure 1 Running example圖1 運行示例

在移動系統中,若一個界程中同時存在2個或2個以上的移動對象,這些移動對象之間視為發生碰撞。例如,在本例中,車輛A和B通過同一界程c7,若車輛A與車輛B在界程c7中的時間有重疊,則車輛A與車輛B將發生碰撞。因此,為避免碰撞事故的發生,有必要為車輛的運行制定調度策略,通過可調度性分析判斷車輛間是否會發生碰撞。
事件和時間是本文的核心概念。在Jiang等人[11,25]提出的模型中,事件指發生的一個行為或一種活動,而事件集則是構成系統的基本元素,事件集與事件集之間相互聯系,存在著選擇、同步、依賴等關系。在現實世界中,事件的執行本身需要耗費一定的時間,另外,2個互相依賴的事件集之間在轉換過程中通常也帶有時間上的延遲。為了描述這些時間約束,本文基于DS模型,在事件集以及事件集之間的轉換中加入時間屬性,提出了時間依賴結構TDS模型。
定義1TDS是一個10元組〈ε,I,T,S,C,W,F,Ti,Te,Tt〉,其中:
(1)ε是有限的事件集合;
(2)I?2ε是初始事件集的集合;
(3)T?2ε?}×2ε?}是所有轉換依賴的集合;
(4)S?2ε是同步關系集,并且滿足?X∈S:|X|>1;
(5)C?2ε是選擇關系集,并且滿足?X∈C:|X|>1;
(6)W:ε→{1,2,3,…}是容量函數;
(7)F?2ε是終止事件集的集合;
(8)Ti:∪X∈IX→Time是初始時間函數;
(9)Te:ε→Time是事件延遲時間函數;
(10)Tt:T→Time是依賴延遲時間函數。

為了方便描述實時移動系統中的時間約束進而通過時間來計算調度,TDS中引入了初始時間函數Ti,用Ti(e)表示初始待執行事件e的初始時鐘值;引入了事件延遲函數Te,用Te(e)表示事件e執行所需的時長。此外,在轉換依賴中,前項事件集和后項事件集之間也可能存在時間延遲,因此TDS中引入依賴延遲時間函數Tt,用Tt((X,Y))來表示轉換依賴(X,Y)執行的時間延遲。
移動系統的運行過程可以表示為TDS中轉換依賴的執行過程,系統的控制條件可以用TDS中的同步關系和選擇關系模擬。在定義系統運行過程之前,為刻畫系統運行過程中的狀態變化,需先定義相應的TDS狀態。
定義2令TDS=〈ε,I,T,S,C,W,F,Ti,Te,Tt〉為時間依賴結構。TDS的狀態為元組S=〈Δ,F,ft,Γ〉,其中:
(1)Δ?ε是當前狀態下的激活事件集,所謂激活事件是指處于可被執行卻尚未被執行的事件。
(2)函數F:Δ→Z*是可用度函數,表示一個事件執行之后被激活的轉換依賴個數,若事件e∈Δ執行后,有n個轉換依賴被激活,則有F(e)=n,n稱為e的可用度值。
(3)ft:Δ→Time是時間函數,對于事件e∈Δ,有ft(e)=t,t稱為當前狀態下e的絕對時間。
(4)Γ?T是當前狀態下激活的轉換依賴集,激活的轉換依賴指可被執行卻尚未被執行的轉換依賴。一個激活的轉換依賴滿足(X,Y)∈Γ?X∈Δ,也即是這類轉換依賴前項事件集中的所有事件在當前狀態下都處于激活狀態。
對任意狀態S=〈Δ,F,ft,Γ〉,也可表示成形如{〈e,F(e),ft(e)〉|e∈Δ}的集合形式。
一個TDS中,存在初始狀態,定義為Si=〈Δi,Fi,fti,Γi},其中激活事件集為Δi=∪X∈IX,可用度函數為?e∈Δi:Fi=|{(X,Y)∈T|e∈X}|,時間函數為?e∈Δi:fti(e)=Ti(e)+Te(e),激活的轉換依賴集為Γi={(X,Y)∈T|X?Δi}。顯然,在初始狀態下,激活狀態集包含了TDS中的所有的初始事件。一個初始事件的絕對時間為該事件的初始時間與該事件的延遲時間之和。
若TDS是有限的,則存在終止狀態,定義為St=〈Δt,Ft,ftt,Γt〉,其中?e∈Δ:e∈F∧Ft(e)=0。也就是說,當一個狀態中所包含的所有激活事件均為終止事件且事件的可用度值都為0時,該TDS將無法繼續運行。因此,該狀態為終止狀態。
一個激活的轉換依賴被執行,意味著該轉換依賴的前項事件集中所有事件被執行,從而導致其后項事件集中的事件被激活,而隨著事件的激活,新的轉換依賴也將被激活,進而使得整個TDS狀態發生轉換。轉換依賴的執行時間由前項事件集中絕對時間最大的事件決定,表示為ttr((X,Y))=max({ft(e)|e∈X}),其中(X,Y)∈T。TDS這一狀態轉換過程實際上定義了TDS的執行語義。
定義3令TDS=〈ε,I,T,S,C,W,F,Ti,Te,Tt〉為時間依賴結構,S1=〈Δ1,F1,ft1,Γ1〉,S2=〈Δ2,F2,ft2,Γ2〉是它的2個狀態。當且僅當以下條件滿足時,S1將通過執行轉換依賴(P,Q)轉換到S2:
(1)(P,Q)∈Γ1。
(2)?/(E,F)∈Γ1:max({ft1(e)|e∈E})+Tt((E,F)) (3)Δ2={e∈Δ1|e?P∨(F1(e)-(1+x)>0∧e∈P)}∪Q。 其中,y=|{(X,Y)∈T|X∩Q≠?}|,x=|{(P,X)∈T|?e∈X,?e′∈Q,?C∈C:e≠e′∧{e,e′}∈C}|。 (5)Γ2=(Γ1({(P,Q)}∪QC))∪QT∪QS,其中QC={(W,X)∈T|W?ε,?e∈X,?e′∈Q,?C∈C:e≠e′∧{e,e′}∈C},QT={(Q,X)|(Q,X)∈T},QS={(X,Y)∈T|X∈S,X?Δ1∪Q,Q?X,Y?ε}。 在上述定義中,條件(1)要求被執行的轉換依賴(P,Q)必須是當前狀態(S1)下激活的轉換依賴。條件(2)要求(P,Q)的執行時間不大于當前狀態下其他任何激活的轉換依賴。條件(3)計算新狀態(S2)下的激活事件,其中包括新激活的事件以及從S1中繼承而來的未被執行過的激活事件。條件(4)計算S2下各個激活事件的可用度值。一旦執行了轉換依賴(P,Q),P中每個事件的可用度值將消耗1+x,其中1表示已執行的轉換依賴(P,Q),x表示由于激活了Q中的事件而被排除掉的轉換依賴的數量。此外,每個激活事件的可用度值應小于或等于其相應的容量值。條件(5)計算S2中激活的轉換依賴,其中包含新激活的轉換依賴與繼承自S1且未被執行過的激活的轉換依賴。條件(6)計算S2中激活事件的絕對時間。上述定義實際上給出了TDS下計算全部狀態的方法。 根據定義3,一個執行時間最小的轉換依賴被執行會導致TDS的狀態發生轉換,而一個狀態中極有可能會同時存在多個執行時間最小且相同的激活的轉換依賴。此時,任意選擇其中的一個轉換依賴來執行,而將余下的轉換依賴留置到新狀態中。這一計算過程將產生過渡狀態。 過渡狀態是TDS中多個激活的轉換依賴具有相同的最小執行時間而導致的過渡產物。為了簡化結果并且更好地建模并發性,本文只使用可達狀態 (非過渡狀態)來描述系統的運行過程。 對于圖1的運行示例,假設車輛A和車輛B通過一個界程需要3個單位時間,車輛C通過一個界程需要2個單位時間;車輛A、B、C進入界程均需1個單位時間,John進入界程需要3個單位時間;車輛A、B、C和John到達路口的初始時間分別為2,0,1和2。該運行示例可建模為:TDSrun=〈ε,I,T,S,C,W,F,Ti,Te,Tt〉(見圖2),其中: Figure 2 TDS model of the running example in figure 1圖2 圖1中運行示例的TDS模型 通過上述討論可知,使用TDS能夠方便地建模移動系統并計算出系統運行過程中各個時刻所處的狀態。然而,僅僅根據狀態仍然無法分析移動對象進出界程的情況,尤其是無法確定多個移動對象進出同一界程的順序。因此,需要引入專門的調度序列來描述移動對象的移動順序。 本節將介紹TDS下的實時調度,并討論其性質。 定義6令TDS=〈ε,I,T,S,C,W,F,Ti,Te,Tt〉為時間依賴結構,如果序列f=S0X1S1…XnSn滿足以下條件: (2)Xi={e∈ε|?(X,Y)∈Di:e∈X},其中i=1,2,…,n。 稱f為TDS的調度全序列,s=X1X2…Xn為TDS的調度序列。為方便描述,定義Sches(TDS)為TDS的所有調度序列的集合。 Table 1 TDS model states of the running example in figure 1表1 圖1中運行示例的可達狀態表 值得一提的是,在智能交通系統中,考慮到車輛的速度與車輛進入系統的初始時間是車輛自帶的屬性,因此在定義實時調度時,只考慮事件執行的先后順序,并未保存事件執行的絕對時間。 □ 定義7令TDS=〈ε,I,T,S,C,W,F,Ti,Te,Tt〉為時間依賴結構,設s1=X1X2…,Xn,s2=Y1Y2…Ym∈Sches(TDS),f1=S0X1S1…XnSn和f2=S′1Y1S′2…YmS′m為TDS的調度全序列。 (2)如果對于調度全序列f1和f2,有Sn=S′1,則s1s2表示s1和s2的組合,即序列X1X2…XnY1Y2…Ym。 該定義表明,一個調度存在子調度,2個滿足(可組合)條件的調度可以組合成一個更大的調度。 在移動系統中,存在多個移動對象經過相同界程的情況。只有當這些移動對象按照一定的先后順序串行地通過該界程時,碰撞才不會發生。由于調度本質上就是系統中的移動對象進入界程的事件集序列,因此通過可調度分析能夠判斷移動對象之間會否相互碰撞。在進行可調度分析之前需引入隔離的概念,作為判斷移動對象是否碰撞的依據。 為方便描述,本節首先定義了3個集合。 e↑s表示包含在調度s中的所有事件的集合,A↑s表示包含在調度s中的所有相關界程的集合,M↑s表示包含在調度s中的所有相關移動對象的集合。 若a、m1、m2滿足以上條件之一,則稱在調度s中移動對象m1與m2在界程a中互相隔離,記為m1Oam2;反之,則稱在調度s中移動對象m1與m2在界程a中互相不隔離,記為m1?am2。 該定義實際上給出了移動系統中移動對象基于事件的隔離。根據先前的討論,一個移動對象通過界程的過程可以用該移動對象的2個相繼的進入事件來表示。定義9實際上涵蓋了移動對象m1與m2在界程a中互相隔離的3種情況:(1)m1和m2均不進入a;(2)m1和m2中的一個進入a;(3)當2個移動對象m1和m2都需要進入界程a時,其中一個移動對象在另一個退出a前不進入a。 定理1令TDS=〈ε,I,T,S,C,W,F,Ti,Te,Tt〉為時間依賴結構,s=X1X2…Xn∈Sches(TDS),a∈A↑s,m1,m2∈M↑s且 a,m1,m2TDS,enm1a,enm2a∈es。 證明 由于在定理1所給的條件下,a,m1,m2不滿足定義9 2個條件中的任意一個,所以m1?am2。 □ 定理1表明,根據給定的調度可以判斷出2個移動對象在某個界程中是否互相不隔離。由于隔離與不隔離是互逆的,因此也可以根據該定理判斷2個移動對象在某個界程中的隔離性。 由以上隔離的定義出發,僅可判斷2個指定的移動對象在某個界程中的隔離性,為了進一步判斷整個移動系統在運行過程中的安全性,還需要在隔離的基礎上對調度進行可調度性分析。 定義10設TDS為時間依賴結構,s=X1X2…Xn∈Sches(TDS)。 (1)當且僅當s滿足條件?m1,m2∈M↑s,?a∈A↑s:m1Oam2時,則稱s是可調度的。 (2)當且僅當s滿足條件時?m1,m2∈M↑s,?a∈A↑s:m1?am2,則稱s是不可調度的。 該定義表明,只有當一個調度中涉及的所有的移動物體在該調度涉及的所有界程中均互相隔離,這一調度才具有可調度性。在一個調度中,只要存在2個相互不隔離的移動對象,則該調度不具有可調度性。 定理2設TDS為時間依賴結構,s=X1X2…Xn為TDS的調度。 □ 定理2實際上是調度的可調度性的一個判定定理,即當且僅當某個調度的所有子調度均可調度時,該調度為可調度的。 定義11設TDS為一個有界的時間依賴結構,s=X1X2…Xn∈Sches(TDS),f=S0X1S1…XnSn為s對應的調度全序列。若S0為TDS的初始狀態,Sn為TDS的終止狀態,則s稱作TDS的完全調度。 該定義表明,一個完全調度是從初始狀態開始直到終止狀態所經歷的所有被執行事件的序列,因此它涵蓋了系統的整個運行過程。只有當TDS有界時,才存在完全調度。 定義12設TDS為有界的時間依賴結構,s=X1X2…Xn為TDS的調度。若s為TDS的完全調度且是可調度的,則稱該TDS為可行的。 通過該定理可知,一個可行的TDS在其運行過程中能夠確保其中的所有移動對象是無碰撞的。 環形交叉路口是一種渠化的交叉路口,在我國,車輛進入環形交叉路口后將按照逆時針方向繞著中心島行駛,從而形成單向交通流。本節將使用TDS來建模一個典型的環形交叉路口的運行場景,并計算對應的實時調度,最后通過可調度分析來判斷該系統是否處于安全狀態。 為簡單起見,本節將建模單車道環形交叉路口,并且只考慮4部車輛進出該路口的情形。如圖3所示,環形交叉路口被分為16個界程(分別編號為c1~c16),路口以外的4個區域分別用x1,x2,x3和x4表示。假設4部車輛進入每個界程均需要1個單位時間。同時假設車輛A、B、C和D到達路口的初始時間分別為1,0,2,2,車輛具有不同的速度,分別需要2,3,4,2個單位時間通過一個界程。對應的時間依賴結構圖如圖4所示,用時間依賴結構描述為: Figure 3 A simple roundabout system圖3 環形交叉路口場景示意圖 Figure 4 TDS model of the roundabout system圖4 環形交叉路口場景的時間依賴結構 TDSrou=〈ε,I,T,S,C,W,F,Ti,Te,Tt〉,其中: S=?,C=?,?e∈ε:W(e)=∞; 根據定義2、定義3以及定義4,可計算出TDSrou的所有可達狀態,為方便后續討論,將所有狀態列入表2。 Table 2 Reachable states of the TDS model in the roundabout system表2 環形交叉路口場景的可達狀態表 由于A↑srou={c1,c2,c3,c4,c5,c6,c7,c8,c9,c10,c11,c12,c13,c14,c15,c16},且M↑srou={A,B,C,D}。在調度全序列frou中,S0是初始狀態,S16是終止狀態。由于B,C∈M↑srou,c16∈A↑srou,B?c16C,因此srou不具有調度性。對應地,TDSrou是不安全的。 基于本文理論,開發了DSTool 工具,該原型工具基于開源圖形庫GoJS,能夠有效地支持模型的圖形化建模,并在此基礎上進行可調度性分析。圖5展示了DSTool的運行界面。 Figure 5 Running interface of DSTool圖5 DSTool運行界面 通過使用DSTool,對前一節的環形交叉路口案例進行了實驗研究(見圖5)。實驗結果表明,基于TDS模型及理論可以快速地計算出移動系統中移動對象之間是否互相隔離,找出將會發生碰撞的移動對象和碰撞的地點,為后續的調度生成提供依據。 本文首先在DS模型的基礎上引入了時間約束,提出了時間依賴結構TDS,并給出了基于TDS的移動系統建模方法;接著為了刻畫移動系統中各移動對象的運行過程定義了實時調度,并研究了實時調度的子調度和調度間的組合;然后為了判斷系統中移動物體間是否發生碰撞,定義了基于事件的隔離并研究了其性質;最后為了確保整個系統的安全性,在隔離理論的基礎上研究了實時調度的可調度性,給出了可調度性的判定定理。實驗結果驗證了上述理論和方法的有效性。在今后的工作中將進一步研究如何快速生成具有可調度性的實時調度策略,并嘗試將該方法應用到實際的智能交通系統中。



4.3 運行示例建模









5 實時調度







6 隔離和可調度性分析
6.1 隔離






6.2 可調度性分析



7 案例和工具
7.1 案例演示













7.2 工具

8 結束語