陳 聰,洪 中,陳楊楊,張 仕,蔣建民,2

(1. 福建師范大學(xué)數(shù)學(xué)與信息學(xué)院，福建 福州 350117；2. 成都信息工程大學(xué)軟件工程學(xué)院，四川 成都 610103)

1 引言

涉及對象運動問題的系統(tǒng)被統(tǒng)稱為移動系統(tǒng)，例如智能交通系統(tǒng)、無人機(jī)、無人船以及多移動機(jī)器人系統(tǒng)[1,2]。保障一個移動系統(tǒng)在運行過程中的安全性是當(dāng)前研究的一個熱點問題。為解決這一問題，首先應(yīng)該確保各個移動對象在運動過程中無碰撞，即各移動對象互相隔離。在移動系統(tǒng)中，由于不同移動對象運行速度和到達(dá)同一區(qū)域的時間存在差異，各個對象將按照一定的序列進(jìn)出這一共同區(qū)域，通過分析該序列即可判斷移動對象之間是否互相隔離。這類序列被稱為調(diào)度序列，而對于給定的調(diào)度序列，分析其是否能夠確保移動對象之間的互相隔離的過程被稱為可調(diào)度性分析。

長期以來，對調(diào)度理論[3 - 8]的研究大多集中于任務(wù)調(diào)度和可調(diào)度性分析。前者主要考慮如何生成最優(yōu)調(diào)度策略，后者則主要驗證一個調(diào)度中是否存在著違反約束條件的情況。早期提出的實時調(diào)度理論側(cè)重于研究可調(diào)度性條件，如原始的單調(diào)速率分析[5]、單調(diào)時限調(diào)度算法[3]和最早截止時間優(yōu)先策略[6]。其后續(xù)研究[4,7,8]則主要集中在信息物理融合系統(tǒng)CPS(Cyber-Physical System)中調(diào)度的優(yōu)化與實現(xiàn)上[9]。作為任務(wù)調(diào)度，它們要求被調(diào)度的任務(wù)之間彼此獨立，互不影響。然而，在移動系統(tǒng)中，由于移動系統(tǒng)與環(huán)境區(qū)域相互作用，很難將一個移動系統(tǒng)分解成多個獨立的任務(wù)，因此使用現(xiàn)有的方法無法直接對移動系統(tǒng)的隔離調(diào)度進(jìn)行建模。

為了解決這個問題，需要一種新的調(diào)度理論來描述移動系統(tǒng)[10,11]中各移動對象的移動過程。Jiang等人[11]提出了一種基于事件的調(diào)度，其中，事件指的是執(zhí)行的一個行為或一個簡單的活動。由于一個任務(wù)可由多個事件來構(gòu)成[9]，基于事件的調(diào)度明顯具有比任務(wù)調(diào)度更細(xì)的粒度。一個復(fù)雜的移動系統(tǒng)，雖然很難將其分解成多個獨立的任務(wù)，但是卻可以輕易地分解為一系列移動事件。因此,它更適用于移動系統(tǒng)中的調(diào)度建模。然而，Jiang等人[11]提出的基于事件的調(diào)度并未考慮時間約束，屬于非實時調(diào)度，為此，本文在該調(diào)度理論的基礎(chǔ)上，加入時間屬性。

要研究移動系統(tǒng)中的實時調(diào)度問題，首先必須對移動系統(tǒng)進(jìn)行建?！，F(xiàn)有的主流的實時形式化方法如時間自動機(jī)[12,13]、時間進(jìn)程代數(shù)[14 - 16]和時間Petri網(wǎng)[17 - 24]等，都無法方便地對移動系統(tǒng)進(jìn)行建模。其中，時間自動機(jī)無法表示移動系統(tǒng)中多個移動對象的并發(fā)行為，而時間進(jìn)程代數(shù)和時間Petri網(wǎng)雖然可以建模并發(fā)行為，但卻不能方便地刻畫移動性[11]。鑒于此，本文引入依賴結(jié)構(gòu)DS(Dependency Structure)[11,25]建模移動系統(tǒng)中的移動對象，刻畫其移動性。然而，模型本身并未考慮時間約束，無法建模移動系統(tǒng)的實時性。為此，本文在DS模型的基礎(chǔ)上增加了時間建模能力，擴(kuò)展出新的模型，稱為時間依賴結(jié)構(gòu)TDS(Time Dependency Structure)。本文將在已有工作[26]的基礎(chǔ)上，從一個典型的智能交通系統(tǒng)入手，進(jìn)一步完善移動系統(tǒng)的建模方法，同時探討基于事件的實時調(diào)度方法，并根據(jù)調(diào)度序列進(jìn)行隔離的可調(diào)度性分析，以確保移動系統(tǒng)運行過程中的安全性。

2 相關(guān)工作

計算機(jī)體系結(jié)構(gòu)的發(fā)展經(jīng)歷了4個主要階段，即：聯(lián)合系統(tǒng)結(jié)構(gòu)、集成的系統(tǒng)結(jié)構(gòu)、系統(tǒng)的體系結(jié)構(gòu)和CPS。為了適應(yīng)體系結(jié)構(gòu)的變化，調(diào)度理論也在不斷發(fā)展。傳統(tǒng)的實時調(diào)度理論是在相應(yīng)的可調(diào)度性條件下發(fā)展起來的，如原始的單調(diào)速率分析[5]、單調(diào)時限調(diào)度算法[3]和最早截止時間優(yōu)先策略[6]。這類調(diào)度理論[3 - 6]大多屬于任務(wù)調(diào)度。而任務(wù)調(diào)度理論是在每個調(diào)度任務(wù)獨立于任何其他任務(wù)這一假設(shè)前提下進(jìn)行研究的，換句話說，在目標(biāo)系統(tǒng)中，嚴(yán)格地要求每個被執(zhí)行的任務(wù)之間不會相互影響。

相比傳統(tǒng)的體系結(jié)構(gòu)，CPS的調(diào)度更為復(fù)雜，因此調(diào)度理論的后續(xù)研究[4,7,8]主要集中在CPS中調(diào)度的優(yōu)化與實現(xiàn)上[9]。Zhang等人[8]研究了一類受反饋控制規(guī)律調(diào)節(jié)的CPS，探討了這類CPS的任務(wù)調(diào)度問題，并針對CPS的可預(yù)測性能和功耗設(shè)計了控制律和任務(wù)調(diào)度算法；Kim等人[27]將Fork-Join并行任務(wù)模型擴(kuò)展到實時CPS中，使其調(diào)度具有實時性，在此基礎(chǔ)上，Kim等人還提出了任務(wù)拉伸變換，使得新興的CPS可以從并行實時任務(wù)中獲得顯著的好處；Schneider等人[28]研究了由硬實時任務(wù)和反饋控制任務(wù)組成的混合關(guān)鍵度信息物理融合系統(tǒng)MCCPS(Mixed-Criticality Cyber-Physical System)的調(diào)度綜合問題，提出了一種MCCPS的多層調(diào)度綜合方案，以便在不同的調(diào)度層中聯(lián)合調(diào)度關(guān)鍵期限任務(wù)和關(guān)鍵任務(wù)；Liu等人[29]深入分析了車載CPS中時態(tài)數(shù)據(jù)分發(fā)的特點，提出了一種基于靜態(tài)快照一致性要求的分析請求服務(wù)時間范圍的算法，即靜態(tài)快照一致性調(diào)度算法；Lee等人[30]提出了一種新的周期性容錯CPS任務(wù)模型，該模型提高了底層物理子系統(tǒng)的效率和穩(wěn)定性；de Martini等人[31]提出了適合于CPS的實時調(diào)度算法，以便最大限度地提高系統(tǒng)利用率，減少調(diào)度開銷，降低上下文切換成本，并對算法進(jìn)行了仿真；Jiang等人[32]研究了基于多智能體系統(tǒng)的分布式最優(yōu)調(diào)度問題，設(shè)計了重新調(diào)度算法，以保證CPS系統(tǒng)在擾動情況下的適應(yīng)性。

從上述工作不難看出,對于調(diào)度理論的研究，一般都是先提出調(diào)度的度量模型，然后基于該度量模型提出調(diào)度算法，最后再對提出的算法進(jìn)行優(yōu)化?？紤]到現(xiàn)有的研究通常是基于傳統(tǒng)的任務(wù)調(diào)度，而任務(wù)調(diào)度要求任務(wù)間互相獨立，因而難以處理更細(xì)粒度的調(diào)度問題。本文提出的基于事件的實時調(diào)度可以將一個任務(wù)拆分成多個互相聯(lián)系的事件，進(jìn)而對事件進(jìn)行調(diào)度，因此更適用于復(fù)雜的移動系統(tǒng)。

3 符號和運行示例

建模移動性需要結(jié)合界程演算[33,34]。界程演算是發(fā)生在封閉且有邊界的界程中的計算，移動對象進(jìn)入或退出界程均屬于界程演算的范疇。在移動系統(tǒng)中創(chuàng)建界程，需要定位設(shè)備與通信技術(shù)的支持，以便將系統(tǒng)大環(huán)境劃分為許多連續(xù)的具有明確邊界的小環(huán)境。每個小環(huán)境被視為一個界程，使用唯一的標(biāo)識符表示。在移動系統(tǒng)中，將一個移動對象進(jìn)入界程定義為進(jìn)入事件，退出界程定義為退出事件，兩者統(tǒng)稱為移動事件。一般而言，使用進(jìn)入和退出這兩類移動事件，便可建模一個移動系統(tǒng)的移動性。例如，一個移動對象通過一個界程的過程可以用相繼執(zhí)行的一個進(jìn)入事件與一個退出事件來表示。由于復(fù)雜的移動系統(tǒng)往往由許多移動對象和界程來組成，系統(tǒng)運行的過程中各個移動對象將不斷地進(jìn)出不同的界程，從而產(chǎn)生連續(xù)的事件序列。

為了幫助讀者理解，圖1給出了一個簡單的智能交通系統(tǒng)的運行示例。該示例描述的是一位乘客John在路口等車并乘車的場景。圖1中的路口區(qū)域被劃分成一系列網(wǎng)格，每個網(wǎng)格被視作一個界程，并且進(jìn)行了編號，將編號為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進(jìn)入界程c6后John進(jìn)入車輛B，然后John隨著車輛B繼續(xù)向前移動。

Figure 1 Running example圖1 運行示例

在移動系統(tǒng)中，若一個界程中同時存在2個或2個以上的移動對象，這些移動對象之間視為發(fā)生碰撞。例如，在本例中，車輛A和B通過同一界程c7，若車輛A與車輛B在界程c7中的時間有重疊，則車輛A與車輛B將發(fā)生碰撞。因此，為避免碰撞事故的發(fā)生，有必要為車輛的運行制定調(diào)度策略，通過可調(diào)度性分析判斷車輛間是否會發(fā)生碰撞。

4 系統(tǒng)模型

事件和時間是本文的核心概念。在Jiang等人[11,25]提出的模型中，事件指發(fā)生的一個行為或一種活動，而事件集則是構(gòu)成系統(tǒng)的基本元素，事件集與事件集之間相互聯(lián)系，存在著選擇、同步、依賴等關(guān)系。在現(xiàn)實世界中，事件的執(zhí)行本身需要耗費一定的時間，另外，2個互相依賴的事件集之間在轉(zhuǎn)換過程中通常也帶有時間上的延遲。為了描述這些時間約束，本文基于DS模型，在事件集以及事件集之間的轉(zhuǎn)換中加入時間屬性，提出了時間依賴結(jié)構(gòu)TDS模型。

4.1 TDS模型的定義

定義1TDS是一個10元組〈ε,I,T,S,C,W,F,Ti,Te,Tt〉，其中：

(1)ε是有限的事件集合；

(2)I?2ε是初始事件集的集合；

(3)T?2ε?}×2ε?}是所有轉(zhuǎn)換依賴的集合；

(4)S?2ε是同步關(guān)系集，并且滿足?X∈S:|X|>1；

(5)C?2ε是選擇關(guān)系集，并且滿足?X∈C:|X|>1；

(6)W:ε→{1,2,3,…}是容量函數(shù)；

(7)F?2ε是終止事件集的集合；

(8)Ti:∪X∈IX→Time是初始時間函數(shù)；

(9)Te:ε→Time是事件延遲時間函數(shù)；

(10)Tt:T→Time是依賴延遲時間函數(shù)。

為了方便描述實時移動系統(tǒng)中的時間約束進(jìn)而通過時間來計算調(diào)度，TDS中引入了初始時間函數(shù)Ti，用Ti(e)表示初始待執(zhí)行事件e的初始時鐘值；引入了事件延遲函數(shù)Te，用Te(e)表示事件e執(zhí)行所需的時長。此外，在轉(zhuǎn)換依賴中，前項事件集和后項事件集之間也可能存在時間延遲，因此TDS中引入依賴延遲時間函數(shù)Tt，用Tt((X,Y))來表示轉(zhuǎn)換依賴(X,Y)執(zhí)行的時間延遲。

4.2 TDS模型的執(zhí)行語義

移動系統(tǒng)的運行過程可以表示為TDS中轉(zhuǎn)換依賴的執(zhí)行過程，系統(tǒng)的控制條件可以用TDS中的同步關(guān)系和選擇關(guān)系模擬。在定義系統(tǒng)運行過程之前，為刻畫系統(tǒng)運行過程中的狀態(tài)變化，需先定義相應(yīng)的TDS狀態(tài)。

定義2令TDS=〈ε,I,T,S,C,W,F,Ti,Te,Tt〉為時間依賴結(jié)構(gòu)。TDS的狀態(tài)為元組S=〈Δ,F,ft,?！?，其中：

(1)Δ?ε是當(dāng)前狀態(tài)下的激活事件集，所謂激活事件是指處于可被執(zhí)行卻尚未被執(zhí)行的事件。

(2)函數(shù)F:Δ→Z*是可用度函數(shù)，表示一個事件執(zhí)行之后被激活的轉(zhuǎn)換依賴個數(shù)，若事件e∈Δ執(zhí)行后，有n個轉(zhuǎn)換依賴被激活，則有F(e)=n,n稱為e的可用度值。

(3)ft:Δ→Time是時間函數(shù)，對于事件e∈Δ，有ft(e)=t,t稱為當(dāng)前狀態(tài)下e的絕對時間。

(4)Γ?T是當(dāng)前狀態(tài)下激活的轉(zhuǎn)換依賴集，激活的轉(zhuǎn)換依賴指可被執(zhí)行卻尚未被執(zhí)行的轉(zhuǎn)換依賴。一個激活的轉(zhuǎn)換依賴滿足(X,Y)∈Γ?X∈Δ，也即是這類轉(zhuǎn)換依賴前項事件集中的所有事件在當(dāng)前狀態(tài)下都處于激活狀態(tài)。

對任意狀態(tài)S=〈Δ,F,ft,Γ〉，也可表示成形如{〈e,F(e),ft(e)〉|e∈Δ}的集合形式。

一個TDS中，存在初始狀態(tài)，定義為Si=〈Δi,Fi,fti,Γi}，其中激活事件集為Δi=∪X∈IX，可用度函數(shù)為?e∈Δi:Fi=|{(X,Y)∈T|e∈X}|，時間函數(shù)為?e∈Δi:fti(e)=Ti(e)+Te(e)，激活的轉(zhuǎn)換依賴集為Γi={(X,Y)∈T|X?Δi}。顯然，在初始狀態(tài)下，激活狀態(tài)集包含了TDS中的所有的初始事件。一個初始事件的絕對時間為該事件的初始時間與該事件的延遲時間之和。

若TDS是有限的，則存在終止?fàn)顟B(tài)，定義為St=〈Δt,Ft,ftt,Γt〉，其中?e∈Δ:e∈F∧Ft(e)=0。也就是說,當(dāng)一個狀態(tài)中所包含的所有激活事件均為終止事件且事件的可用度值都為0時，該TDS將無法繼續(xù)運行。因此，該狀態(tài)為終止?fàn)顟B(tài)。

一個激活的轉(zhuǎn)換依賴被執(zhí)行，意味著該轉(zhuǎn)換依賴的前項事件集中所有事件被執(zhí)行，從而導(dǎo)致其后項事件集中的事件被激活，而隨著事件的激活，新的轉(zhuǎn)換依賴也將被激活，進(jìn)而使得整個TDS狀態(tài)發(fā)生轉(zhuǎn)換。轉(zhuǎn)換依賴的執(zhí)行時間由前項事件集中絕對時間最大的事件決定，表示為ttr((X,Y))=max({ft(e)|e∈X})，其中(X,Y)∈T。TDS這一狀態(tài)轉(zhuǎn)換過程實際上定義了TDS的執(zhí)行語義。

定義3令TDS=〈ε,I,T,S,C,W,F,Ti,Te,Tt〉為時間依賴結(jié)構(gòu)，S1=〈Δ1,F1,ft1,Γ1〉,S2=〈Δ2,F2,ft2,Γ2〉是它的2個狀態(tài)。當(dāng)且僅當(dāng)以下條件滿足時，S1將通過執(zhí)行轉(zhuǎn)換依賴(P,Q)轉(zhuǎn)換到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)要求被執(zhí)行的轉(zhuǎn)換依賴(P,Q)必須是當(dāng)前狀態(tài)(S1)下激活的轉(zhuǎn)換依賴。條件(2)要求(P,Q)的執(zhí)行時間不大于當(dāng)前狀態(tài)下其他任何激活的轉(zhuǎn)換依賴。條件(3)計算新狀態(tài)(S2)下的激活事件，其中包括新激活的事件以及從S1中繼承而來的未被執(zhí)行過的激活事件。條件(4)計算S2下各個激活事件的可用度值。一旦執(zhí)行了轉(zhuǎn)換依賴(P,Q),P中每個事件的可用度值將消耗1+x，其中1表示已執(zhí)行的轉(zhuǎn)換依賴(P,Q),x表示由于激活了Q中的事件而被排除掉的轉(zhuǎn)換依賴的數(shù)量。此外，每個激活事件的可用度值應(yīng)小于或等于其相應(yīng)的容量值。條件(5)計算S2中激活的轉(zhuǎn)換依賴，其中包含新激活的轉(zhuǎn)換依賴與繼承自S1且未被執(zhí)行過的激活的轉(zhuǎn)換依賴。條件(6)計算S2中激活事件的絕對時間。上述定義實際上給出了TDS下計算全部狀態(tài)的方法。

根據(jù)定義3，一個執(zhí)行時間最小的轉(zhuǎn)換依賴被執(zhí)行會導(dǎo)致TDS的狀態(tài)發(fā)生轉(zhuǎn)換，而一個狀態(tài)中極有可能會同時存在多個執(zhí)行時間最小且相同的激活的轉(zhuǎn)換依賴。此時，任意選擇其中的一個轉(zhuǎn)換依賴來執(zhí)行，而將余下的轉(zhuǎn)換依賴留置到新狀態(tài)中。這一計算過程將產(chǎn)生過渡狀態(tài)。

過渡狀態(tài)是TDS中多個激活的轉(zhuǎn)換依賴具有相同的最小執(zhí)行時間而導(dǎo)致的過渡產(chǎn)物。為了簡化結(jié)果并且更好地建模并發(fā)性，本文只使用可達(dá)狀態(tài) (非過渡狀態(tài))來描述系統(tǒng)的運行過程。

4.3 運行示例建模

對于圖1的運行示例，假設(shè)車輛A和車輛B通過一個界程需要3個單位時間，車輛C通過一個界程需要2個單位時間；車輛A、B、C進(jìn)入界程均需1個單位時間，John進(jìn)入界程需要3個單位時間；車輛A、B、C和John到達(dá)路口的初始時間分別為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模型

5 實時調(diào)度

通過上述討論可知，使用TDS能夠方便地建模移動系統(tǒng)并計算出系統(tǒng)運行過程中各個時刻所處的狀態(tài)。然而，僅僅根據(jù)狀態(tài)仍然無法分析移動對象進(jìn)出界程的情況，尤其是無法確定多個移動對象進(jìn)出同一界程的順序。因此，需要引入專門的調(diào)度序列來描述移動對象的移動順序。 本節(jié)將介紹TDS下的實時調(diào)度，并討論其性質(zhì)。

定義6令TDS=〈ε,I,T,S,C,W,F,Ti,Te,Tt〉為時間依賴結(jié)構(gòu)，如果序列f=S0X1S1…XnSn滿足以下條件：

(2)Xi={e∈ε|?(X,Y)∈Di:e∈X},其中i=1,2,…,n。

稱f為TDS的調(diào)度全序列，s=X1X2…Xn為TDS的調(diào)度序列。為方便描述，定義Sches(TDS)為TDS的所有調(diào)度序列的集合。

Table 1 TDS model states of the running example in figure 1表1 圖1中運行示例的可達(dá)狀態(tài)表

值得一提的是，在智能交通系統(tǒng)中，考慮到車輛的速度與車輛進(jìn)入系統(tǒng)的初始時間是車輛自帶的屬性，因此在定義實時調(diào)度時，只考慮事件執(zhí)行的先后順序，并未保存事件執(zhí)行的絕對時間。

□

定義7令TDS=〈ε,I,T,S,C,W,F,Ti,Te,Tt〉為時間依賴結(jié)構(gòu)，設(shè)s1=X1X2…,Xn,s2=Y1Y2…Ym∈Sches(TDS),f1=S0X1S1…XnSn和f2=S′1Y1S′2…YmS′m為TDS的調(diào)度全序列。

(2)如果對于調(diào)度全序列f1和f2，有Sn=S′1，則s1s2表示s1和s2的組合，即序列X1X2…XnY1Y2…Ym。

該定義表明，一個調(diào)度存在子調(diào)度，2個滿足(可組合)條件的調(diào)度可以組合成一個更大的調(diào)度。

6 隔離和可調(diào)度性分析

在移動系統(tǒng)中,存在多個移動對象經(jīng)過相同界程的情況。只有當(dāng)這些移動對象按照一定的先后順序串行地通過該界程時，碰撞才不會發(fā)生。由于調(diào)度本質(zhì)上就是系統(tǒng)中的移動對象進(jìn)入界程的事件集序列，因此通過可調(diào)度分析能夠判斷移動對象之間會否相互碰撞。在進(jìn)行可調(diào)度分析之前需引入隔離的概念，作為判斷移動對象是否碰撞的依據(jù)。

6.1 隔離

為方便描述，本節(jié)首先定義了3個集合。

e↑s表示包含在調(diào)度s中的所有事件的集合,A↑s表示包含在調(diào)度s中的所有相關(guān)界程的集合,M↑s表示包含在調(diào)度s中的所有相關(guān)移動對象的集合。

若a、m1、m2滿足以上條件之一，則稱在調(diào)度s中移動對象m1與m2在界程a中互相隔離，記為m1Oam2；反之，則稱在調(diào)度s中移動對象m1與m2在界程a中互相不隔離，記為m1?am2。

該定義實際上給出了移動系統(tǒng)中移動對象基于事件的隔離。根據(jù)先前的討論，一個移動對象通過界程的過程可以用該移動對象的2個相繼的進(jìn)入事件來表示。定義9實際上涵蓋了移動對象m1與m2在界程a中互相隔離的3種情況：(1)m1和m2均不進(jìn)入a；(2)m1和m2中的一個進(jìn)入a；(3)當(dāng)2個移動對象m1和m2都需要進(jìn)入界程a時，其中一個移動對象在另一個退出a前不進(jìn)入a。

定理1令TDS=〈ε,I,T,S,C,W,F,Ti,Te,Tt〉為時間依賴結(jié)構(gòu)，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表明，根據(jù)給定的調(diào)度可以判斷出2個移動對象在某個界程中是否互相不隔離。由于隔離與不隔離是互逆的，因此也可以根據(jù)該定理判斷2個移動對象在某個界程中的隔離性。

6.2 可調(diào)度性分析

由以上隔離的定義出發(fā)，僅可判斷2個指定的移動對象在某個界程中的隔離性，為了進(jìn)一步判斷整個移動系統(tǒng)在運行過程中的安全性，還需要在隔離的基礎(chǔ)上對調(diào)度進(jìn)行可調(diào)度性分析。

定義10設(shè)TDS為時間依賴結(jié)構(gòu)，s=X1X2…Xn∈Sches(TDS)。

(1)當(dāng)且僅當(dāng)s滿足條件?m1,m2∈M↑s,?a∈A↑s:m1Oam2時，則稱s是可調(diào)度的。

(2)當(dāng)且僅當(dāng)s滿足條件時?m1,m2∈M↑s,?a∈A↑s:m1?am2，則稱s是不可調(diào)度的。

該定義表明，只有當(dāng)一個調(diào)度中涉及的所有的移動物體在該調(diào)度涉及的所有界程中均互相隔離，這一調(diào)度才具有可調(diào)度性。在一個調(diào)度中，只要存在2個相互不隔離的移動對象，則該調(diào)度不具有可調(diào)度性。

定理2設(shè)TDS為時間依賴結(jié)構(gòu)，s=X1X2…Xn為TDS的調(diào)度。

□

定理2實際上是調(diào)度的可調(diào)度性的一個判定定理，即當(dāng)且僅當(dāng)某個調(diào)度的所有子調(diào)度均可調(diào)度時，該調(diào)度為可調(diào)度的。

定義11設(shè)TDS為一個有界的時間依賴結(jié)構(gòu)，s=X1X2…Xn∈Sches(TDS),f=S0X1S1…XnSn為s對應(yīng)的調(diào)度全序列。若S0為TDS的初始狀態(tài)，Sn為TDS的終止?fàn)顟B(tài)，則s稱作TDS的完全調(diào)度。

該定義表明，一個完全調(diào)度是從初始狀態(tài)開始直到終止?fàn)顟B(tài)所經(jīng)歷的所有被執(zhí)行事件的序列，因此它涵蓋了系統(tǒng)的整個運行過程。只有當(dāng)TDS有界時，才存在完全調(diào)度。

定義12設(shè)TDS為有界的時間依賴結(jié)構(gòu)，s=X1X2…Xn為TDS的調(diào)度。若s為TDS的完全調(diào)度且是可調(diào)度的，則稱該TDS為可行的。

通過該定理可知，一個可行的TDS在其運行過程中能夠確保其中的所有移動對象是無碰撞的。

7 案例和工具

7.1 案例演示

環(huán)形交叉路口是一種渠化的交叉路口，在我國，車輛進(jìn)入環(huán)形交叉路口后將按照逆時針方向繞著中心島行駛，從而形成單向交通流。本節(jié)將使用TDS來建模一個典型的環(huán)形交叉路口的運行場景，并計算對應(yīng)的實時調(diào)度，最后通過可調(diào)度分析來判斷該系統(tǒng)是否處于安全狀態(tài)。

為簡單起見，本節(jié)將建模單車道環(huán)形交叉路口，并且只考慮4部車輛進(jìn)出該路口的情形。如圖3所示，環(huán)形交叉路口被分為16個界程(分別編號為c1～c16)，路口以外的4個區(qū)域分別用x1,x2,x3和x4表示。假設(shè)4部車輛進(jìn)入每個界程均需要1個單位時間。同時假設(shè)車輛A、B、C和D到達(dá)路口的初始時間分別為1,0,2,2，車輛具有不同的速度,分別需要2,3,4,2個單位時間通過一個界程。對應(yīng)的時間依賴結(jié)構(gòu)圖如圖4所示，用時間依賴結(jié)構(gòu)描述為:

Figure 3 A simple roundabout system圖3 環(huán)形交叉路口場景示意圖

Figure 4 TDS model of the roundabout system圖4 環(huán)形交叉路口場景的時間依賴結(jié)構(gòu)

TDSrou=〈ε,I,T,S,C,W,F,Ti,Te,Tt〉，其中:

S=?,C=?,?e∈ε:W(e)=∞;

根據(jù)定義2、定義3以及定義4，可計算出TDSrou的所有可達(dá)狀態(tài)，為方便后續(xù)討論，將所有狀態(tài)列入表2。

Table 2 Reachable states of the TDS model in the roundabout system表2 環(huán)形交叉路口場景的可達(dá)狀態(tài)表

由于A↑srou={c1,c2,c3,c4,c5,c6,c7,c8,c9,c10,c11,c12,c13,c14,c15,c16},且M↑srou={A,B,C,D}。在調(diào)度全序列frou中，S0是初始狀態(tài)，S16是終止?fàn)顟B(tài)。由于B,C∈M↑srou,c16∈A↑srou,B?c16C，因此srou不具有調(diào)度性。對應(yīng)地，TDSrou是不安全的。

7.2 工具

基于本文理論，開發(fā)了DSTool 工具，該原型工具基于開源圖形庫GoJS，能夠有效地支持模型的圖形化建模，并在此基礎(chǔ)上進(jìn)行可調(diào)度性分析。圖5展示了DSTool的運行界面。

Figure 5 Running interface of DSTool圖5 DSTool運行界面

通過使用DSTool，對前一節(jié)的環(huán)形交叉路口案例進(jìn)行了實驗研究(見圖5)。實驗結(jié)果表明，基于TDS模型及理論可以快速地計算出移動系統(tǒng)中移動對象之間是否互相隔離，找出將會發(fā)生碰撞的移動對象和碰撞的地點，為后續(xù)的調(diào)度生成提供依據(jù)。

8 結(jié)束語

本文首先在DS模型的基礎(chǔ)上引入了時間約束，提出了時間依賴結(jié)構(gòu)TDS，并給出了基于TDS的移動系統(tǒng)建模方法；接著為了刻畫移動系統(tǒng)中各移動對象的運行過程定義了實時調(diào)度，并研究了實時調(diào)度的子調(diào)度和調(diào)度間的組合；然后為了判斷系統(tǒng)中移動物體間是否發(fā)生碰撞，定義了基于事件的隔離并研究了其性質(zhì)；最后為了確保整個系統(tǒng)的安全性，在隔離理論的基礎(chǔ)上研究了實時調(diào)度的可調(diào)度性，給出了可調(diào)度性的判定定理。實驗結(jié)果驗證了上述理論和方法的有效性。在今后的工作中將進(jìn)一步研究如何快速生成具有可調(diào)度性的實時調(diào)度策略，并嘗試將該方法應(yīng)用到實際的智能交通系統(tǒng)中。