文獻調(diào)研報告模板

1、安全關鍵系統(tǒng)通信協(xié)議調(diào)研報告（2015.4.12）1 調(diào)研題目安全關鍵系統(tǒng)通信協(xié)議的建模與分析2 任務說明對本次調(diào)研任務的具體說明1) 查閱國外的相關文獻；2) 補充通信協(xié)議中的具體網(wǎng)絡；3) 閱讀標準EN50159；3 關鍵字檢索詞：CBTC；安全關鍵系統(tǒng)；安全通信協(xié)議；EN50159；safety communication protocol檢索策略：無線*通信；總線*通信；以太網(wǎng)*通信；CBTC*communication protocol；safety*protocol；verification/ test/ model / simulation / design / analysis

2、 *(safety) communication protocol; 4 檢索范圍中國知網(wǎng) 百度 httpweb of science(SCIE) /IEEE Springer LINK ELSEVIER ScienceDirect(SDOL) 在不同關鍵詞組合下，檢索范圍內(nèi)，近三年的文獻總數(shù)5 主要的檢索文獻對重點文獻的說明1 BS EN50159 Railway applicationsCommunication, signaling and processing systems- Safety- related communication in transm

3、ission systemsS.2 安全通信與安全通信標準EN50159J. 鐵路通信信號工程技術，2014.3 Performance evaluation and verification of communication protocol for railway signaling systems J. Computer Standards & Interfaces, 2005.4 Verification and conformance test generation of communication protocol for railway signaling systems J.

4、Computer Standards & Interfaces, 2007.5 Development of verification and conformance testing tools for a railway signaling communication protocol J. Computer Standards & Interfaces, 2009.4 Group communication on highways: An evaluation study of geocast protocols and applicationsJ.Ad Hoc Networks, 201

5、3.6 Compositional verification of a communication protocol for a remotely operated aircraftC. Science of Computer Programming, 2013.7 Verification of the safety communication protocol in train control system using colored Petri netJ. Reliability Engineering and System Safety, 2012.(國內(nèi)-陳黎潔)8 Simulati

6、on and verification of RSSP-II safety communication protocolC. 2012 Second International Conference on Business Computing and Global Information, 2012.(國內(nèi)-許孟華)9 Formal verification of safety protocol in train control system J. Technological Sciences, 2011 (國內(nèi)-北交團隊)10 無線傳感器網(wǎng)絡安全通信協(xié)議研究與設計D.碩士，大連理工大學，20

7、06.11 安全關鍵實時通信協(xié)議研究D.博士，蘭州大學，2011.12 基于ZigBee的無線傳感器網(wǎng)絡通信協(xié)議棧設計與實現(xiàn)D.碩士，電子科技大學，2009.13 基于工業(yè)以太網(wǎng)的列車通信網(wǎng)絡研究D.碩士，北京交通大學，2011.6 檢索結果摘要匯總自己要著重解釋的文獻信息，文獻格式可以適當簡化根據(jù)以上檢索范圍與檢索關鍵詞，其中部分檢索結果5篇，摘述如下：【篇名】安全通信與安全通信標準EN50159【作者】楊劍【期刊名稱】鐵路通信信號工程技術【年份】2014年2月，第11卷第1期【摘要】EN50159是歐洲鐵路通信信號領域信息傳輸系統(tǒng)中安全通信標準。對安全通信基本知識進行一般介紹，對最新版本E

8、N50159:2010標準內(nèi)容進行簡單解讀，并結合自身實踐，對安全通信協(xié)議軟件開發(fā)相關經(jīng)驗要點進行介紹。【篇名】Development of verification and conformance testing tools for a railway signaling communication protocol【作者】Jae-Ho Lee, Jong-Gyu Hwang, Ducko Shin, Kang-Mi Lee, Sung-Un Kim【期刊名稱】Computer Standards & Interfaces【年份】2009【摘要】Verification and confor

9、mance testing for protocol specification, the key part of the protocol development process, are complementary technologies employed to increase confidence that a system will function as stated in its specifications. In this paper, we verify the safety and liveness of the protocol specified for the L

10、abeled Transition System (LTS) by using model-checking method and implementing the testing tool, which experimentally demonstrates the presence of deadlock and reachability from the initial state to a random state. Implementing the testing tool can use modal mu-calculus to assess whether protocol mo

11、del properties, presented by modal logic, meet protocol specifications. In addition, we propose a conformance testing tool to check correct implementation of sequences that have been derived by the UIO method from the specification of the protocol being verified. This generating tool uses the C+ lan

12、guage in the Microsoft Windows NT environment.【篇名】Compositional verification of a communication protocol for a remotely operated aircraft【作者】Alwyn E. Goodloe, Csar A. Mu?oz【期刊類型】Science of Computer Programming【年份】2013【摘要】This paper presents the formal specification and verification of a communicatio

13、n protocol between a ground station and a remotely operated aircraft. The protocol can be seen as the vertical composition of protocol layers, where each layer performs input and output message processing, and the horizontal composition of different processes concurrently inhabiting the same layer,

14、where each process should satisfy a distinct delivery requirement. A compositional technique is used to formally prove that the protocol satisfies these requirements. Although the protocol itself is not novel, the methodology employed in its verification extends existing techniques by automating the

15、 tedious and usually cumbersome part of the proof, thereby making the iterative design process of protocols feasible.【篇名】基于工業(yè)以太網(wǎng)的列車通信網(wǎng)絡研究【作者】張建斌【學位類型】碩士【授予單位】北京交通大學【導師】譚南林【年份】2011【摘要】:傳統(tǒng)以太網(wǎng)通信的非實時和非確定性限制了其在列車通信網(wǎng)絡中應用。改變以太網(wǎng)通信驅(qū)動和調(diào)度機制可使之成為適合列車通信的實時以太網(wǎng)。本文深入研究了影響以太網(wǎng)實時性和確定性通信的因素后提出了解決方案,并在設計的實驗平臺上進行了驗證。本文以星

16、型網(wǎng)絡為基礎研究了共享式和交換式以太網(wǎng)的實時特性,得出交換式以太網(wǎng)符合列車通信網(wǎng)絡組網(wǎng)要求。分析了時間觸發(fā)架構的通信機制并引入以太網(wǎng)中,分時復用的通信方法保證了以太網(wǎng)的通信的實時性和確定性,在此基礎上提出以太網(wǎng)確定性通信的調(diào)度機制,并分析計算了通信網(wǎng)絡的宏觀調(diào)度周期。為了建立基于時間觸發(fā)機制的以太網(wǎng)通信網(wǎng)絡,本文在IEEEI588時鐘同步協(xié)議基礎上,提出了一種新的從時鐘時間補償方法即漸近時間補償法,解決了直接補償算法的時間“突變”問題,為驗證算法的合理性和科學性,用MATLAB對時鐘同步過程進行了建模分析。在以太網(wǎng)技術基礎上研究了以太網(wǎng)通信節(jié)點可行性設計方案。完成了兩類以太網(wǎng)通信節(jié)點硬件設計,

17、移植了實時操作系統(tǒng)和TCP/IP協(xié)議棧,搭建了交換式以太網(wǎng)通信的實驗平臺,以實驗平臺為基礎,實現(xiàn)了IEEEI588時鐘同步協(xié)議棧,建立了時鐘同步網(wǎng)絡。最后,為考察通信網(wǎng)絡的實時響應能力和時鐘同步精度,本文設計了通信網(wǎng)絡的測試方案,對通信網(wǎng)絡平臺的通信性能進行了定量分析?！酒炕赯igBee的無線傳感器網(wǎng)絡通信協(xié)議棧設計與實現(xiàn)【作者】李蔚【學位類型】碩士【授予單位】電子科技大學【導師】童玲【年份】2012【摘要】無線傳感器網(wǎng)絡技術應用前景非常廣闊,在醫(yī)療、農(nóng)業(yè)、環(huán)境、軍事、侵入監(jiān)測、軌跡跟蹤、機器故障等不同應用領域開始顯現(xiàn)出了巨大的潛力。無線傳感器網(wǎng)絡中的通信協(xié)議棧屬于網(wǎng)絡底層關鍵技術之一,

18、是通信系統(tǒng)中不可分割的重要組成部分,是使得傳感器網(wǎng)絡應用能夠進行交互的關鍵所在。本文基于ZigBee技術提出了一種可移植性強、提供良好編程接口的無線傳感器網(wǎng)絡通信協(xié)議棧的設計與實現(xiàn),其目的是為了降低開發(fā)傳感器網(wǎng)絡應用的難度,同時也可為研究人員研究無線傳感器網(wǎng)絡效能、改進通信協(xié)議提供一個堅實基礎。本文設計的無線傳感器網(wǎng)絡通信協(xié)議棧具有理論和應用上的意義。本文著重介紹了協(xié)議棧的MAC層、網(wǎng)絡層的設計與實現(xiàn)。設計實現(xiàn)的MAC層在數(shù)據(jù)服務上支持直接傳輸與間接傳輸,支持CSMA/CA機制接入信道;在管理上,支持信道的掃描、數(shù)據(jù)請求、關聯(lián)等功能。網(wǎng)絡層支持網(wǎng)絡的建立、加入、離開、網(wǎng)絡地址分配等網(wǎng)絡管理功能

19、,支持網(wǎng)絡數(shù)據(jù)的單播及廣播服務等數(shù)據(jù)服務功能。網(wǎng)絡層的路由管理支持多對一、分級路由、最小路由成本等路由策略。本文在以射頻芯片CC2531為核心硬件平臺上,進行了協(xié)議棧的性能指標測試:MAC層主要進行鏈路的數(shù)據(jù)傳輸吞吐量與丟幀率等性能指標的測試;網(wǎng)絡層主要進行自組織網(wǎng)絡能力、路由算法反應能力、端對端網(wǎng)絡時延及傳輸成功率等性能指標的測試。7 調(diào)研結果分析自己的思考和心得7.1 國外相關研究1 Development of verification and conformance testing tools for a railway signaling commun- ication protoc

20、olJ. Computer Standards & Interfaces,2009.論文的主要工作就是采用label transition system（LTS）和輸入/輸出有限狀態(tài)機（I/O FSM）來描述了一個通信協(xié)議，并驗證鐵路信號通信協(xié)議的安全性和活性，驗證方法是算子（mu-calculus）和模型檢測(model checking)，這其中的一致性測試、UIO序列、測試生成方法都是依據(jù)I/O FSM 中層模型來實現(xiàn)的。論文中指出協(xié)議驗證包括在實施協(xié)議之前檢查用戶需求與協(xié)議是否匹配，分析協(xié)議規(guī)范是否正確等。4 Group communication on highways: An ev

21、aluation study of geocast protocols and applicationsJ.Ad Hoc Networks, 2013.該論文針對高速道路交通系統(tǒng)的安全通信需求,提出一種DBA MAC (Dynamic Backbone Assisted MAC)協(xié)議,通過模型分析、仿真學習等方法得到信噪比、通信延時等QoS參數(shù)，并與傳統(tǒng)的geocast協(xié)議相比，仿真結果證明可以該協(xié)議可以作為高速道路交通系統(tǒng)中的安全通信協(xié)議。5 Compositional verification of a communication protocol for a remotely opera

22、ted aircraftC. Science of Computer Programming, 2013.該論文主要對遙控飛行系統(tǒng)和地面站之間的安全通信協(xié)議進行組合驗證，從而對協(xié)議整體安全性進行驗證。為了對通信協(xié)議進行安全性驗證，首先要對其進行各種規(guī)范和狀態(tài)的定義，這里用到的PVS是一種緊密耦合的規(guī)范語言，也是一種交互式的定理證明器。接著將協(xié)議分為應用層、傳輸層、鏈路層和介質(zhì)層,每一層都單獨執(zhí)行輸入和輸出消息的處理，并且每一層的傳輸過程都應該滿足不同的信息傳輸要求。這里用PVS表示不同層的行為和狀態(tài),從而驗證其安全性。7.2 EN50159學習該標準中沒有對通信協(xié)議的基本框架有規(guī)定，也未對安全

23、通信協(xié)議的具體內(nèi)涵和要求有規(guī)定。歐洲電工標準化委員會(CENELEC)制定了網(wǎng)絡傳輸系統(tǒng)安全通信標準EN50159，該標準適用于為了通信使用封閉或開放傳輸系統(tǒng)的安全相關電子系統(tǒng)。為在連接到傳輸系統(tǒng)的安全相關設備之間達成安全相關的通信，該標準給出了所需的基本要求（并不是專門針對安全通信協(xié)議）。早期公布的版本中分為EN50159-1:2001和EN50159-2:2001兩部分。EN50159-1定義了封閉傳輸系統(tǒng)中的安全通信標準,而EN50159-2則定義了開放傳輸系統(tǒng)中的安全通信標準。2010年9月的最新版本的EN50159:2010標準中,將兩部分合成一部分,統(tǒng)稱為傳輸系統(tǒng)的安全通信標準。E

24、N50159:2010中對開放傳輸系統(tǒng)的劃分更為詳細,依據(jù)是否存在未經(jīng)授權的接入的風險,分為免于此風險的開放傳輸系統(tǒng)及承受此風險的開放傳輸系統(tǒng)。封閉式傳輸系統(tǒng)的特點為:1)存在已知最大數(shù)量的可連接參與者;2)傳輸系統(tǒng)的特點已知,媒介已知或固定;3)只允許經(jīng)過批準的訪問。開放式傳輸系統(tǒng)的特點為:1)依據(jù)既定流程讀取、存儲、處理或重新傳輸用戶數(shù)據(jù)的元素是用戶未知的;用戶的數(shù)量一般是未知的,安全相關的和非安全相關的,以及和鐵路應用不相關的設備都可連接到該傳輸系統(tǒng)中;2)傳輸介質(zhì)的傳輸特性和磁化率所受外部環(huán)境的影響是未知的;3)網(wǎng)絡控制和管理系統(tǒng)能夠通過該傳輸系統(tǒng)兩端的任何一種或多于一種類型的傳輸介質(zhì)

25、,按照用戶未知的程序發(fā)送(動態(tài)重新發(fā)送)消息;4)未知的其他傳輸系統(tǒng)中的用戶能夠以未知的形式發(fā)送未知量的信息。EN50159-1標準提出了系統(tǒng)為了滿足功能完整性，所應該采取的保護措施和手段。提出了為滿足安全完整性、安全相關設備之間通信和通信鏈路所需的安全性、安全，所應該滿足的安全要求。該標準還提出對系統(tǒng)安全代碼的要求。EN50159-2標準中還指出了傳輸系統(tǒng)可能遭受的威脅以及防御措施。標準中建議運用序列號、時間戳、源地址和目的地址標識、超時防護、反饋消息、身份鑒別以及加密技術,來防御遇到的威脅。提出了對傳輸系統(tǒng)的消息防護要求（包括通用要求、特定防護等）。在附錄部分，該標準給出了使用安全代碼和加

26、密技術的注意事項和應用建議?？偟脕碚f，EN50159標準化鐵路信號安全相關通信功能與技術規(guī)范,對安全相關系統(tǒng)的設計具有指導意義。EN50159標準制定了系統(tǒng)傳輸過程中的威脅與防御手段,提出在安全相關設備之間進行信息交換、消息傳遞的過程中,需要進行安全編碼、安全傳輸以及安全校驗等安全相關通信過程。安全通信在系統(tǒng)結構上,就是將安全編碼與解碼的安全層插入到傳輸層與應用層之間。安全設備之間傳遞的用戶報文由應用層傳遞給安全層進行安全編碼,將生成的安全報文通過傳輸層傳輸;接收端接收到報文,也要通過安全層解碼、校驗后過濾后才被采用。而在EN50159:2010中闡述的安全通信參考架構即為在應用層與傳輸系統(tǒng)間

27、建立安全層。標準中將傳輸系統(tǒng)帶來的安全隱患總結為潛在的報文錯誤,安全層的建立應能有效防御報文錯誤,為安全相關數(shù)據(jù)的傳輸提供保障。具體到安全層采取的安全措施則取決于傳輸系統(tǒng)的類型。用戶數(shù)據(jù)首先經(jīng)安全層處理,生成安全層數(shù)據(jù)報文后再經(jīng)由傳輸系統(tǒng)發(fā)送。從傳輸系統(tǒng)接收到的信息也先經(jīng)過安全層過濾再被采用。從邏輯角度講,安全層對應用層、傳輸系統(tǒng)是透明的,無論傳輸系統(tǒng)釆用何種結構及協(xié)議棧,安全相關數(shù)據(jù)都能在安全層的保護下抵達目的地。7.3 通信協(xié)議中的網(wǎng)絡（1）現(xiàn)場總線（field bus）現(xiàn)場總線是指現(xiàn)場儀表和數(shù)字控制系統(tǒng)輸入輸出之間的全數(shù)字化、雙向、多站的通訊系統(tǒng)。現(xiàn)場總線是將自動化最底層的現(xiàn)場控制器和現(xiàn)

28、場智能儀表設備互連的實時控制通訊網(wǎng)絡，遵循ISO的OSI開放系統(tǒng)互連參考模型的全部或部分通訊協(xié)議。目前已經(jīng)開發(fā)出有40多種現(xiàn)場總線，它們分別應用在不同的行業(yè)領域。較流行的有5種，分別是FF、Profitbus、HART、CAN和LonWorks。盡管目前有多種可用的現(xiàn)場總線，但其并沒有被廣泛的應用于安全關鍵系統(tǒng)中，因其開發(fā)過程中并沒有融入安全的設計理念，而是在實現(xiàn)完成后，再去推到其設計的安全性。作為一種涌現(xiàn)特征，安全性不可能在系統(tǒng)部署之后被添加進去，它必須貫穿于系統(tǒng)的整個開發(fā)過程中。因此若要將現(xiàn)場總線應用于安全關鍵系統(tǒng)，應將安全管理概念貫穿于協(xié)議設計開發(fā)和驗證過程中，從過程中保證與安全標準的兼

29、容性以提高系統(tǒng)的安全置信度。工業(yè)用現(xiàn)場總線的拓撲方式主要有總線型、星型、環(huán)型、樹型等，不同的組網(wǎng)方式有各自不同的優(yōu)缺點。其中星型拓撲結構中所有的通信節(jié)點都連接在一個中心設備上,刪除或移動某個節(jié)點都比較方便,某個節(jié)點發(fā)生故障,不會影響到整個網(wǎng)絡,中心節(jié)點是整個網(wǎng)絡的關鍵,要求具有很高的可靠性和安全性。（2）工業(yè)以太網(wǎng)現(xiàn)場總線技術誕生后，實時通信網(wǎng)絡技術被廣泛的用于工業(yè)控制領域，如上面內(nèi)容所示，有40多種不同的現(xiàn)場總線應用在不同的行業(yè)領域。與此同時，工業(yè)以太網(wǎng)成為現(xiàn)場總線研究和應用的新熱點，并涌現(xiàn)了大量的工業(yè)以太網(wǎng)實時通信協(xié)議應用于工業(yè)控制領域。雖然相比于現(xiàn)場總線技術,以太網(wǎng)具有普遍性,低成本,高帶寬等特性。但是同時傳統(tǒng)以太網(wǎng)是一種非確定性、非實時性的網(wǎng)絡系統(tǒng)，會造成數(shù)據(jù)傳輸?shù)牟淮_定性，無法滿足安全關鍵系統(tǒng)信息傳輸對于網(wǎng)絡的高實時性和確定性的要求。同時最初以太網(wǎng)的設計也沒有考慮到安全關鍵系統(tǒng)工業(yè)現(xiàn)場的特殊應用環(huán)境，也無法保證通信網(wǎng)絡的可靠性和穩(wěn)定性。為了滿足實時性和穩(wěn)定性要求，同時降低成本，部分實