• <tr id="yyy80"></tr>
  • <sup id="yyy80"></sup>
  • <tfoot id="yyy80"><noscript id="yyy80"></noscript></tfoot>
  • 99热精品在线国产_美女午夜性视频免费_国产精品国产高清国产av_av欧美777_自拍偷自拍亚洲精品老妇_亚洲熟女精品中文字幕_www日本黄色视频网_国产精品野战在线观看 ?

    基于混成自動機(jī)的城市軌道交通ZC子系統(tǒng)建模與驗證方法

    2016-03-30 03:00:42黃友能張鵬基侯曉鵬
    中國鐵道科學(xué) 2016年2期
    關(guān)鍵詞:自動機(jī)子系統(tǒng)線性

    黃友能,張鵬基,侯曉鵬,唐 濤

    (1.北京交通大學(xué) 電子信息工程學(xué)院,北京 100044;2.北京交通大學(xué) 軌道交通運行控制系統(tǒng)國家工程研究中心,北京 100044)

    基于通信的列車控制系統(tǒng)(Communication Based Train Control,CBTC)是保證城市軌道交通列車安全、高效運行的系統(tǒng),其區(qū)域控制器(Zone Controller,ZC)子系統(tǒng)主要實現(xiàn)為管轄范圍內(nèi)列車計算移動授權(quán)(Movement Authority,MA)、區(qū)域控制器邊界切換等功能[1],這些功能的安全性是保障行車安全的基礎(chǔ),因此針對ZC子系統(tǒng)功能的安全驗證就顯得尤為重要。

    ZC子系統(tǒng)主要通過無線傳輸方式接收車載子系(Vital OnBoard Computer,VOBC)的信息,因此在車地通信過程中不可避免會出現(xiàn)信號延遲或發(fā)送失敗等情況,同時,由于ZC子系統(tǒng)在同一時間段內(nèi)會與管轄范圍內(nèi)的所有列車進(jìn)行交互,因此要求該系統(tǒng)應(yīng)具有較強(qiáng)的并發(fā)性與實時性。另外,ZC子系統(tǒng)在計算移動授權(quán)的過程中,需要考慮列車連續(xù)變化參數(shù)(距離、速度和加速度等)的演化過程,以及設(shè)備交互的一些離散事件,具有明顯的混成特性[2]。

    關(guān)于列車控制系統(tǒng)安全驗證的既有研究工作,有的針對系統(tǒng)的并發(fā)性與實時性進(jìn)行建模與驗證,如同濟(jì)大學(xué)的徐中偉教授等利用Petri網(wǎng)模型和故障樹實現(xiàn)了對聯(lián)鎖軟件的安全性評估等[3],但缺少相應(yīng)的驗證環(huán)節(jié)。有的針對系統(tǒng)混成特性進(jìn)行研究,如北京交通大學(xué)的呂繼東博士利用混合通信進(jìn)程對系統(tǒng)進(jìn)行建模仿真,但缺少相應(yīng)的驗證軟件[4]。北京交通大學(xué)的劉金濤博士利用動態(tài)微分邏輯形式化語言對CTCS-3級列車控制系統(tǒng)進(jìn)行了仿真與驗證,但驗證過程需要大量的推導(dǎo)公式,效率和重用性都較低。

    本文基于形式化建模驗證理論[5-6],結(jié)合統(tǒng)一建模語言(Unified Modelling Language,UML)的交互流程描述能力和自定義擴(kuò)展能力,針對ZC子系統(tǒng)的混成特性,建立ZC子系統(tǒng)的UML順序圖;采用模型轉(zhuǎn)換方法,定義從源模型到目標(biāo)模型的轉(zhuǎn)換規(guī)則,將ZC子系統(tǒng)的UML順序圖轉(zhuǎn)換為線性混成自動機(jī)模型,用于ZC子系統(tǒng)功能的安全驗證;以實際的ZC子系統(tǒng)邊界切換控制功能場景為例,根據(jù)建立的ZC子系統(tǒng)線性混成自動機(jī)模型,采用形式化工具BACH(Bounded reachability checker)對該場景的7條功能性質(zhì)和4條安全性質(zhì)進(jìn)行驗證。

    1 功能場景建模方法

    針對ZC子系統(tǒng)具有連續(xù)變量(距離、速度和加速度等)的動態(tài)特性,首先采用UML順序圖描述系統(tǒng)的實時交互特性,然后利用UML的標(biāo)記值和約束的擴(kuò)展方式對順序圖進(jìn)行擴(kuò)展,給出模型轉(zhuǎn)換的定義及規(guī)則,使源模型與目標(biāo)模型的語義相同,將順序圖轉(zhuǎn)換為線性混成自動機(jī)模型。

    1.1 UML順序圖擴(kuò)展

    為了能夠表達(dá)ZC子系統(tǒng)的混成特性,需要對UML順序圖進(jìn)行擴(kuò)展[7]。將順序圖中的消息發(fā)送和消息接收采用事件表示,利用標(biāo)記值和約束的擴(kuò)展方式,對順序圖進(jìn)行了以下2個方面的擴(kuò)展。

    1)對時間的擴(kuò)展

    (1)事件上添加時鐘及其約束(可有多個時鐘),即本事件在什么時間范圍內(nèi)發(fā)生;

    (2)事件上添加時鐘變化率恒為1(以1 ms為時間單位長度);

    (3)動作的時間約束,即只有滿足時間約束時動作才會發(fā)生;

    (4)動作的時鐘重置,即動作完成時要進(jìn)行時鐘重置。

    2)對連續(xù)變量的擴(kuò)展

    (1)事件上添加變量的約束(可有多個變量),即本事件發(fā)生時變量的變化范圍;

    (2)事件上添加變量的變化率(可為實數(shù)范圍如[0.9,1.1]);

    (3)動作的變量約束,即只有滿足變量約束時動作才會發(fā)生;

    (4)動作的變量賦值,即動作完成時要進(jìn)行的變量賦值。

    圖1 UML擴(kuò)展內(nèi)容展示

    1.2 線性混成自動機(jī)定義

    以Alur提出的定義框架為基準(zhǔn)[8],對線性混成自動機(jī)作如下定義。

    定義1

    線性混成自動機(jī)(Linear Hybrid Automata)形式為

    H:(X,Y,V,E,V0,fflow,iinv,iinit)

    其中各個參數(shù)的含義如下。

    X:實數(shù)值系統(tǒng)變量的有限集合,X={x1,x2,…,xn},其中n為變量的個數(shù),也被稱為自動機(jī)的維度(dimension)。

    Y:動作名有限集合。

    V:位置節(jié)點的有限集合。

    V0:初始位置節(jié)點集合。

    1.3 模型轉(zhuǎn)換的定義、規(guī)則和步驟

    1.3.1模型轉(zhuǎn)換的定義

    UML順序圖定義了多種類型的交互片段,這些交互片段組成了UML順序圖的不同生命線即對象間的活動。本文在此基礎(chǔ)上增加定義了單元片段,用于刻畫比較簡單的消息傳遞過程。按照該定義,交互片段也可看作是由眾多單元片段按照一定規(guī)則組合而成的。

    定義1:

    單元片段語義表示為1個或多個可視的事件序列,每個單元片段由相應(yīng)的單個或多個事件序列組成。事件e1和e2間的關(guān)系應(yīng)當(dāng)滿足以下3種關(guān)系之一。

    (1)在初始事件中,e1為消息發(fā)送事件,則e2為相對應(yīng)的消息接收事件。

    (2)若在同一實例的生命線上,事件e1出現(xiàn)在e2之前,則e1是消息發(fā)送事件;并且事件e1和e2可作為可視對(e1,e2)。

    (3)若在同一實例的生命線上,事件e1出現(xiàn)在事件e2之后,則e2是消息發(fā)送事件。

    定義2:

    1個單元片段是1個8元數(shù)據(jù)組,可表示為UF(I,W,M,Z,B,C,G,J)。

    其中各參數(shù)的含義如下。

    I:對象的有限集合。

    W:事件的有限集合,W*為包括空事件串在內(nèi)的所有不重復(fù)事件串集合,p為事件串集合,?p∈H*,|p|為p的字符個數(shù),p(n)為p中的第n個事件,2個事件用“.”連接。

    M:有窮的動作集合,包括消息的接收與發(fā)送。

    Z:可視對事件集合,Z={e,e′}代表1個可視對。

    B:事件約束集合(包括時間與變量)。

    C:事件間約束集合(包括時間與變量)。

    G:事件標(biāo)簽值集合(時間與變量的變化率)。

    J:消息賦值集合。

    1.3.2模型轉(zhuǎn)換的規(guī)則

    1)單元片段轉(zhuǎn)換規(guī)則

    將單元片段進(jìn)行轉(zhuǎn)換,得到目標(biāo)單元自動機(jī)A(N,n0,L)。

    UF(I,W,M,Z,B,C,G,J)→A(N,n0,L)

    其中各參數(shù)的含義如下。

    N:節(jié)點集合,N={p,d,r},其中,p∈W*,并且對于∶?j

    n0:集合N的1個空狀態(tài)。在每個單元片段上都建立1個空狀態(tài),以便后期的組合優(yōu)化。

    L:目標(biāo)單元自動機(jī)事件集合,L={l′,g,m,a,l},與混成自動機(jī)轉(zhuǎn)換關(guān)系集合E相對應(yīng),其中l(wèi)′和l為自動機(jī)的2個節(jié)點對應(yīng)于UML中可視事件對,且l′,l∈N;g為遷移條件,即進(jìn)行狀態(tài)跳變時變量需要滿足的條件,是UML圖中接收發(fā)送消息需要滿足的時間或變量條件的擴(kuò)展;m為動作集合,對應(yīng)于UML圖中消息的發(fā)送與接收;a為動作過程中賦值更新的集合,對應(yīng)于UML圖中動作的時間重置與變量賦值更新擴(kuò)展。

    2)組合片段轉(zhuǎn)換規(guī)則

    規(guī)則1:在1個多分支交互片段“Alt”中有q個互斥的可選分支,每個分支上都有執(zhí)行該分支的“使能”條件,只有條件為真的分支才被執(zhí)行,每個分支是1個單元片段或者組合片段。

    定義函數(shù)Alt(g,AF), 其中g(shù)為對應(yīng)可選分支的門條件,AF為所有可選片段的集合, 則可按照以下規(guī)則得到自動機(jī)AAlt(N,n0,L)。

    Alt(g,AF)→AAlt(N,n0,L)

    其中

    N={n0}∪N1∪N2…

    L={〈n0,ε,guard1,ε,n1,0〉,〈n0,ε,guard2,ε,n2,0〉}…∪L1∪L2…

    式中:N1和N2為節(jié)點集合N的子集合;guard1和guard2為所要滿足條件集合guard中的子條件;n1,0和n2,0為集合N的另外2個空狀態(tài);L1和L2為有限集合L的子集合。

    圖2為有2種選擇的Alt組合片段轉(zhuǎn)換規(guī)則示意圖,圖中A,B,C為組合片段的組合對象;A1和A2為子自動機(jī)。

    圖2 組合片段Alt轉(zhuǎn)換規(guī)則示意圖

    規(guī)則2: 1個組合片段Opt是1種單選擇行為,這種單選擇行為類似于Alt組合片段中的某種行為。

    定義選擇片段函數(shù)Opt(OF),其中OF為單分支選擇片段變量,可按照以下規(guī)則得到自動機(jī)AOpt(N,n0,L)。

    Opt(OF)→AOpt(N,n0,L)

    其中

    L={〈n0,ε,guard1,ε,n1,0〉,〈n0,ε,else,ε,

    n2,0〉}∪L1∪L2

    式中:else為除guard外需要滿足的其他條件。

    圖3為1個組合片段Opt的轉(zhuǎn)換規(guī)則示意圖。

    圖3 組合片段Opt轉(zhuǎn)換規(guī)則示意圖

    規(guī)則3:1個組合片段Loop表示1種循環(huán)行為,組合片段中的子片段會被不斷重復(fù)直到不滿足條件為止。

    設(shè)函數(shù)Loop(LF,guard), 其中LF為所要不斷重復(fù)的子片段,guard為所要滿足的條件, 則可按照以下規(guī)則得到自動機(jī)ALoop(N,n0,L)。

    Loop(LF,guard)→ALoop(N,n0,L)

    其中

    N={n0,ne}∪N1

    L={〈n0,ε,guard,ε,n1,0〉,〈n0,ε,!guard,ε,ne〉}∪L1

    式中:ne為集合N的1個新的空狀態(tài);e為自然數(shù)。

    圖4是1個組合片段loop轉(zhuǎn)化規(guī)則示意圖,圖中A1為需要循環(huán)片段構(gòu)造的子自動機(jī)。

    圖4 組合片段Loop轉(zhuǎn)換規(guī)則示意圖

    規(guī)則4:多個組合片段可組成1個完整的自動機(jī),組合片段按照生命線由上到下的順序執(zhí)行。

    設(shè)函數(shù)Combin(CF), 其中CF為所有的組合片段,guard為所要滿足的條件,則可按照以下規(guī)則得到自動機(jī)ACombin(N,n0,L)。

    Combin(CF)→ACombin(N,n0,L)

    其中,

    N=N1∪N2…

    n0=n1,0

    L={〈ni,e,ε,ε,ε,ni+1,0〉}∪L1∪L2

    (1≤i≤m-1)

    式中:ni,e為集合N的另外的空狀態(tài),i和e均為自然數(shù)。

    1.3.3模型轉(zhuǎn)換的步驟

    在得到1個擴(kuò)展的UML順序圖之后,經(jīng)過以下4步將其轉(zhuǎn)換為目標(biāo)線性混成自動機(jī)。

    Step1:將擴(kuò)展后的UML順序圖根據(jù)時間先后順序拆分為不同組合片段,由于組合片段內(nèi)可能會嵌套著其他組合片段和單元片段,需要將組合片段繼續(xù)拆分,直至將整個順序圖拆分為單元片段。

    Step2:根據(jù)單元片段轉(zhuǎn)換規(guī)則,將單元片段轉(zhuǎn)換為目標(biāo)單元自動機(jī)。

    Step3:根據(jù)組合片段轉(zhuǎn)換規(guī)則,將1個組合片段對應(yīng)的多個單元片段都轉(zhuǎn)換成目標(biāo)單元自動機(jī),然后再組合成該組合片段對應(yīng)的線性混成自動機(jī)。

    Step4:根據(jù)拆分組合片段時的順序,將不同組合片段的線性混成自動機(jī)合成為完整的目標(biāo)線性混成自動機(jī)模型。

    2 ZC子系統(tǒng)建模與驗證案例

    針對CBTC系統(tǒng)的混成特性,根據(jù)北京地鐵亦莊線ZC邊界切換工程數(shù)據(jù)選取列車在小紅門ZC與亦莊橋ZC邊界切換控制功能場景進(jìn)行具體建模與驗證。ZC通信周期為400ms,VOBC通信周期為200 ms。

    2.1 ZC邊界切換控制功能場景分析

    當(dāng)列車從1個ZC管轄區(qū)域進(jìn)入另一個ZC管轄區(qū)域時,ZC將根據(jù)移交ZC發(fā)送的移動MA判斷列車是否已經(jīng)運行到地面區(qū)域分界點,如果已經(jīng)到達(dá)地面區(qū)域分界點,則由移交ZC向接管ZC發(fā)出移交列車申請,此后由這2個ZC分別計算列車在各自管轄范圍內(nèi)的MA,并由當(dāng)前控制列車ZC負(fù)責(zé)將這2部分MA信息混合后發(fā)送給列車。在車地通信正常的情況下,列車將接收到MA,并根據(jù)移動授權(quán)計算速度曲線;如列車在5 s內(nèi)仍接收不到新的MA,將認(rèn)為在ZC切換過程中發(fā)生了車地通信故障,列車將觸發(fā)緊急制動,使列車在車地通信故障前接收到的移動授權(quán)終點前停車。

    列車從小紅門ZC管轄區(qū)域進(jìn)入亦莊橋ZC管轄區(qū)域時,越區(qū)切換的具體過程可以分為以下5個階段。

    階段1:如圖5所示,列車在小紅門ZC區(qū)域內(nèi)運行,當(dāng)MA終點為小紅門ZC區(qū)域與亦莊橋ZC區(qū)域邊界點JZ9時,此時小紅門ZC(移交ZC)將與亦莊橋ZC(接管ZC)通信,觸發(fā)邊界切換控制功能。

    圖5 ZC邊界切換觸發(fā)控制圖

    階段2:在車地通信正常的情況下,如圖6所示,隨著列車的運行,移交ZC為列車計算移動授權(quán)MA1,接管ZC為列車計算移動授權(quán)MA2,由于此時列車仍受到移交ZC控制,移交ZC將MA1和MA2的信息混合后向列車發(fā)送“終點至H點”的移動授權(quán)。

    圖6 車地通信正常情況下ZC邊界切換控制圖

    階段3:當(dāng)列車車頭位置越過ZC邊界JZ9時,此時移交ZC為列車計算移動授權(quán)MA1,接管ZC為列車計算移動授權(quán)MA2,列車受接管ZC的控制,由接管ZC將MA1和MA2的信息混合后向列車發(fā)送“終點至H點”的移動授權(quán)。

    階段4:在列車車尾越過ZC邊界JZ9時,將向移交ZC發(fā)送注銷申請,并根據(jù)接管ZC發(fā)送的移動授權(quán)完成行車作業(yè)。假如列車車尾在越過ZC邊界JZ9時前方有障礙物等情況,則計算安全制動曲線并根據(jù)曲線完成停車過程。

    階段5:在車地通信故障的情況下,如圖7所示,列車將觸發(fā)緊急制動,列車在H點前停車。

    圖7 車地通信故障情況下ZC邊界切換控制圖

    2.2 ZC邊界切換控制功能場景建模

    首先定義參數(shù),見表1。

    表1 參數(shù)定義表

    針對ZC邊界切換控制功能場景,采用擴(kuò)展的UML順序圖,建立ZC邊界切換控制功能場景的UML順序圖;根據(jù)車地通信的5個階段,將建立的UML順序圖分為5個組合片段;以其中1個組合片段1為例,其UML順序圖如圖8所示。

    根據(jù)模型轉(zhuǎn)換的定義和規(guī)則,將圖8所示的UML順序圖轉(zhuǎn)換為單元自動機(jī);將所有的單元自動機(jī)根據(jù)轉(zhuǎn)換的先后順序組合成線性混成自動機(jī)模型,如圖9所示。

    2.3 驗證及結(jié)果分析

    本文利用線性混成自動機(jī)的形式化驗證軟件BACH對該場景的功能性質(zhì)和安全性質(zhì)進(jìn)行驗證。BACH是南京大學(xué)設(shè)計開發(fā)的面向線性混成系統(tǒng)有界可達(dá)性的模型驗證軟件,它將BMC思想擴(kuò)展到了線性混成自動機(jī)的可達(dá)性檢驗工作中。該工具主要檢驗功能有:單元自動機(jī)面向路徑可達(dá)性驗證;單自動機(jī)有界可達(dá)性驗證;自動機(jī)組系統(tǒng)面向路徑組可達(dá)性驗證;自動機(jī)組系統(tǒng)有界可達(dá)性驗證。本文主要運用后2種驗證功能。

    根據(jù)圖9所示的ZC邊界切換控制功能線性混成自動機(jī)模型,采用BACH模型驗證軟件提供的可以針對每個成員自動機(jī)分別建立模型的功能,分別建立該具體場景下VOBC,移交ZC和接管ZC的線性混成自動機(jī)模型,如圖10所示。

    圖8 ZC邊界切換控制功能場景部分UML順序圖

    圖9 ZC邊界切換控制功能場景線性混成自動機(jī)模型

    圖10 VOBC,移交ZC和接管ZC的線性混成自動機(jī)模型

    通過BACH軟件中檢測模塊CLHA Checker對場景模型進(jìn)行功能性驗證。利用檢測模塊CLHA Checker中的Path-Oriented Reachability選項先對模型中自動機(jī)組的路徑可達(dá)性進(jìn)行檢測,然后針對ZC子系統(tǒng)邊界切換場景的7條功能性質(zhì)進(jìn)行驗證。檢測路徑及驗證結(jié)果如表2所示。

    利用檢測模塊CLHA Checker中的Bounded Reachability選項對自動機(jī)組的有界可達(dá)性進(jìn)行檢測。在有界可達(dá)性的檢測過程中加入各個對象的線性混成自動機(jī)編碼文本。為了驗證列車安全性能,在VOBC線性混成自動機(jī)模型中加入減速狀態(tài)和超速狀態(tài),選擇終點目標(biāo)節(jié)點,然后根據(jù)目標(biāo)節(jié)點選擇待可達(dá)性的檢查節(jié)點進(jìn)行有界可達(dá)性檢測。檢測完成后再針對4條安全性質(zhì)進(jìn)行驗證,安全性質(zhì)及驗證結(jié)果見表3。

    表2 功能性質(zhì)驗證

    表3 安全性質(zhì)驗證

    在考慮了ZC邊界切換控制中車地通信正常以及故障2種情況的基礎(chǔ)上,通過表2中的7條路徑可達(dá)性性質(zhì)驗證可以看出,ZC邊界切換控制功能符合設(shè)計要求;通過表3中4條有界可達(dá)性安全性質(zhì)驗證可以看出,在ZC邊界切換控制功能場景下,列車能夠安全通過地面區(qū)域邊界點,也沒有超速情況,且能夠在接管ZC管轄范圍內(nèi)安全停車。但由于本案例在設(shè)計之初將障礙物的位置設(shè)置的距離邊界點較近,使得在ZC切換過程中,列車尚未完全通過邊界點就開始降速停車了。在將障礙物位置后移之后,通過檢測發(fā)現(xiàn)減速狀態(tài)可達(dá),說明列車能夠安全通過地面區(qū)域邊界點且無降速,符合安全需求。

    3 結(jié) 論

    本文針對ZC子系統(tǒng)具有混成性的特點,利用擴(kuò)展后的UML順序圖對ZC子系統(tǒng)進(jìn)行建模;采用模型轉(zhuǎn)換方法,定義從源模型到目標(biāo)模型的轉(zhuǎn)換規(guī)則,將ZC子系統(tǒng)的UML順序圖模型轉(zhuǎn)換為形式化的線性混成自動機(jī)模型,用于ZC子系統(tǒng)功能的安全驗證。以北京地鐵亦莊線ZC邊界切換控制功能場景為例,建立該場景的UML順序圖;將其對應(yīng)車地通信的5個階段細(xì)分為5個組合片段;根據(jù)模型轉(zhuǎn)換定義及規(guī)則,進(jìn)一步將各組合片段拆分為單元片段,將1個組合片段對應(yīng)的多個單元片段轉(zhuǎn)換成目標(biāo)單元自動機(jī)后,再合成該組合片段對應(yīng)的線性混成自動機(jī);根據(jù)拆分組合片段時的順序,將不同組合片段的線性混成自動機(jī)合成為完整的目標(biāo)線性混成自動機(jī)模型。根據(jù)建立的線性混成自動機(jī)模型,采用驗證工具BACH對該場景的7條功能性質(zhì)和4條安全性質(zhì)進(jìn)行驗證。結(jié)果表明:ZC邊界切換控制功能滿足設(shè)計要求,列車能夠安全通過地面區(qū)域邊界點,沒有超速情況且能夠在接管ZC管轄范圍內(nèi)安全停車。表明所提出的建模和驗證方法是可行的,彌補(bǔ)了對具有混成特性列車控制系統(tǒng)既有驗證方法的不足。

    [1]唐濤,郜春海,黃友能,等. CJ/T 407—2012 城市軌道交通基于通信的列車自動控制系統(tǒng)技術(shù)要求[S].北京:中國標(biāo)準(zhǔn)出版社,2012.

    (TANG Tao,GAO Chunhai, HUANG Youneng,et al. CJ/T 407—2012 Technical Requirement of Communication Based Automatic Train Control System for Urban Rail Transit[S].Beijing:China Standard Press,2012.in Chinese)

    [2]劉金濤,唐濤,趙林,等. 基于微分動態(tài)邏輯的無線閉塞中心交接協(xié)議建模與驗證[J].中國鐵道科學(xué),2012,33(5):98-104.

    (LIU Jintao,TANG Tao,ZHAO Lin,et al. Modeling and Verification of Radio Block Center Handover Protocol Based on Differential Dynamic Logic[J]. China Railway Science,2012,33(5):98-104.in Chinese)

    [3]杜軍威, 徐中偉, 王樹梅. 聯(lián)鎖邏輯模型的安全性分析[J].計算機(jī)工程與應(yīng)用,2007,43(2):1-4.

    (DU Junwei, XU Zhongwei,WANG Shumei. Safety Analysis of Interlocking Logic Model[J]. Computer Engineering and Applications, 2007,43(2):1-4.in Chinese)

    [4]呂繼東. 列車運行控制系統(tǒng)分層形式化建模與驗證分析[D]. 北京:北京交通大學(xué), 2011.

    (Lü Jidong, Hierarchical Formal Modeling and Verification Train Control System[D].Beijing:Beijing Jiaotong University,2011.in Chinese)

    [5]PLATZER A′e,QUESEL Jan-David. European Train Control System: a Case Study in Formal Verification[J]. Lecture Notes in Computer Science,2009,5885:246-265.

    [6]WERNER Damm, ALFRED Mikschl, JENS Oehlerking, et al. Automating Verification of Cooperation, Control and Design in Traffic Applications[J]. Lecture Notes in Computer Science,2007,4770:115-169.

    [7]ONJECT Management Group. Unified Modeling Language:Super Structure[EB/OL].2013-07-30[2015-04-15]. http://www.omg.org.

    [8]ALURA R,COURCOUBETIS C,HALBWACHS N,et al.The Algorithmic Analysis of Hybrid Systems[J]. Theoretical Computer Science, 1995, 138(94):3-34.

    猜你喜歡
    自動機(jī)子系統(tǒng)線性
    不對中轉(zhuǎn)子系統(tǒng)耦合動力學(xué)特性研究
    漸近線性Klein-Gordon-Maxwell系統(tǒng)正解的存在性
    {1,3,5}-{1,4,5}問題與鄰居自動機(jī)
    線性回歸方程的求解與應(yīng)用
    GSM-R基站子系統(tǒng)同步方案研究
    一種基于模糊細(xì)胞自動機(jī)的新型疏散模型
    智富時代(2019年4期)2019-06-01 07:35:00
    駝峰測長設(shè)備在線監(jiān)測子系統(tǒng)的設(shè)計與應(yīng)用
    二階線性微分方程的解法
    廣義標(biāo)準(zhǔn)自動機(jī)及其商自動機(jī)
    車載ATP子系統(tǒng)緊急制動限制速度計算
    长治县| 汪清县| 文登市| 拉萨市| 兴山县| 九龙县| 镶黄旗| 璧山县| 日喀则市| 山东省| 裕民县| 利津县| 谷城县| 潮州市| 关岭| 乐业县| 津南区| 罗山县| 夏河县| 杭锦旗| 东平县| 同仁县| 宁河县| 玛沁县| 永登县| 贡觉县| 崇仁县| 巴东县| 蓬安县| 雷州市| 怀安县| 枣庄市| 长春市| 温州市| 体育| 普兰店市| 利津县| 马鞍山市| 津市市| 潼关县| 霍城县|