移動(dòng)系統(tǒng)的實(shí)時(shí)調(diào)度與可調(diào)度性分析*

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

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

1 引言

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

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

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

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

2 相關(guān)工作

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

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

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

3 符號(hào)和運(yùn)行示例

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

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

Figure 1 Running example圖1 運(yùn)行示例

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

4 系統(tǒng)模型

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

4.1 TDS模型的定義

定義1TDS是一個(gè)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í)間函數(shù)；

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

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

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

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

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

定義2令TDS=〈ε,I,T,S,C,W,F,Ti,Te,Tt〉為時(shí)間依賴結(jié)構(gòu)。TDS的狀態(tài)為元組S=〈Δ,F,ft,?！担渲校?/p>

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

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

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

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

對(duì)任意狀態(tài)S=〈Δ,F,ft,?！担部杀硎境尚稳鐊〈e,F(e),ft(e)〉|e∈Δ}的集合形式。

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

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

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

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

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

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

4.3 運(yùn)行示例建模

對(duì)于圖1的運(yùn)行示例，假設(shè)車輛A和車輛B通過(guò)一個(gè)界程需要3個(gè)單位時(shí)間，車輛C通過(guò)一個(gè)界程需要2個(gè)單位時(shí)間；車輛A、B、C進(jìn)入界程均需1個(gè)單位時(shí)間，John進(jìn)入界程需要3個(gè)單位時(shí)間；車輛A、B、C和John到達(dá)路口的初始時(shí)間分別為2,0,1和2。該運(yùn)行示例可建模為：TDSrun=〈ε,I,T,S,C,W,F,Ti,Te,Tt〉(見(jiàn)圖2)，其中：

Figure 2 TDS model of the running example in figure 1圖2 圖1中運(yùn)行示例的TDS模型

5 實(shí)時(shí)調(diào)度

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

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

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

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

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

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

□

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

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

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

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

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

6.1 隔離

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

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

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

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

定理1令TDS=〈ε,I,T,S,C,W,F,Ti,Te,Tt〉為時(shí)間依賴結(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個(gè)條件中的任意一個(gè)，所以m1?am2。

□

定理1表明，根據(jù)給定的調(diào)度可以判斷出2個(gè)移動(dòng)對(duì)象在某個(gè)界程中是否互相不隔離。由于隔離與不隔離是互逆的，因此也可以根據(jù)該定理判斷2個(gè)移動(dòng)對(duì)象在某個(gè)界程中的隔離性。

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

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

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

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

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

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

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

□

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

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

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

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

通過(guò)該定理可知，一個(gè)可行的TDS在其運(yùn)行過(guò)程中能夠確保其中的所有移動(dòng)對(duì)象是無(wú)碰撞的。

7 案例和工具

7.1 案例演示

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

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

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

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

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

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

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

Table 2 Reachable states of the TDS model in the roundabout system表2 環(huán)形交叉路口場(chǎng)景的可達(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)度性。對(duì)應(yīng)地，TDSrou是不安全的。

7.2 工具

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

Figure 5 Running interface of DSTool圖5 DSTool運(yùn)行界面

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

8 結(jié)束語(yǔ)

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