楚 敏 邵振洲 王 瑞 李曉娟 張 芮

(首都師范大學(xué)信息工程學(xué)院 北京 100048)(輕型工業(yè)機(jī)器人與安全驗(yàn)證北京市重點(diǎn)實(shí)驗(yàn)室(首都師范大學(xué)) 北京 100048)

0 引 言

ROS是一個(gè)用于機(jī)器人軟件開發(fā)的開源操作系統(tǒng)[1]。ROS為機(jī)器人應(yīng)用提供了統(tǒng)一的接口標(biāo)準(zhǔn)，容易與其他的機(jī)器人軟件平臺(tái)集成。ROS中執(zhí)行某一任務(wù)的進(jìn)程稱為節(jié)點(diǎn)，機(jī)器人控制系統(tǒng)通常由多個(gè)節(jié)點(diǎn)組成。節(jié)點(diǎn)之間傳遞消息的主要方式是主題。主題通信方式通過(guò)發(fā)布者發(fā)布主題，訂閱者訂閱主題來(lái)進(jìn)行。但是，在ROS的通信過(guò)程中，存在一些安全隱患。例如，節(jié)點(diǎn)的活動(dòng)不受限制，任何節(jié)點(diǎn)都可以進(jìn)行注冊(cè)和主題發(fā)布。攻擊者可以很容易地偽造節(jié)點(diǎn)來(lái)發(fā)布假消息，并竊聽重要主題的消息。另一方面，通信數(shù)據(jù)缺乏實(shí)時(shí)監(jiān)控，異常消息無(wú)法被捕獲。因此，需要建立合理的安全監(jiān)控機(jī)制保護(hù)節(jié)點(diǎn)通信過(guò)程的安全。這對(duì)于提高機(jī)器人系統(tǒng)的安全性和可靠性具有重要意義。

運(yùn)行時(shí)驗(yàn)證[2]是一種輕量級(jí)的驗(yàn)證方法，采用形式化的方式對(duì)系統(tǒng)行為規(guī)范進(jìn)行描述。它實(shí)時(shí)監(jiān)控系統(tǒng)程序的運(yùn)行軌跡，判斷系統(tǒng)行為是否違反安全規(guī)范。該方法與模型檢測(cè)[3]和定理證明方法[4]相比，復(fù)雜度更低。與傳統(tǒng)的測(cè)試方法相比，運(yùn)行時(shí)驗(yàn)證在對(duì)屬性的描述以及對(duì)程序的監(jiān)控方面具有靈活性和擴(kuò)展性。運(yùn)行時(shí)驗(yàn)證已經(jīng)應(yīng)用在ROS系統(tǒng)安全性保障中，Huang[5]提出了一個(gè)ROSRV框架，該框架可以監(jiān)控消息數(shù)據(jù)，并可選地修改消息內(nèi)容，但是并未對(duì)程序進(jìn)行邏輯驗(yàn)證。Balsa-Comerón等[6]認(rèn)為ROS中的主要安全問(wèn)題是明文通信，提出對(duì)通信數(shù)據(jù)使用對(duì)稱加密算法。但是，密鑰的管理和泄露會(huì)帶來(lái)隱患。其他學(xué)者針對(duì)ROS通信安全提出了其他策略，如White等[7]通過(guò)TLS(傳輸層安全加密協(xié)議)對(duì)兩個(gè)通信應(yīng)用程序之間的隱私和數(shù)據(jù)完整性進(jìn)行了保護(hù)，Breiling等[8]提出建立一個(gè)安全的傳輸信道，使ROS節(jié)點(diǎn)能夠更加安全的通信。

本文基于運(yùn)行時(shí)驗(yàn)證技術(shù)，針對(duì)ROS操作系統(tǒng)在主題通信和節(jié)點(diǎn)活動(dòng)方面存在的安全問(wèn)題，提出了一個(gè)ROS-Monitor監(jiān)控框架。該框架支持時(shí)序邏輯描述系統(tǒng)安全屬性，根據(jù)自定義場(chǎng)景生成監(jiān)控器來(lái)監(jiān)控系統(tǒng)行為。若系統(tǒng)行為違背安全屬性，則打印相關(guān)告警信息。

1 背景知識(shí)

1.1 ROS[1,9]的通信方式

主題通信是ROS節(jié)點(diǎn)進(jìn)行消息通信的主要方式，圖1展示了ROS主題通信的機(jī)制與過(guò)程[10]。它通過(guò)一系列XML/RPC(一種用于遠(yuǎn)程過(guò)程調(diào)用協(xié)議)請(qǐng)求來(lái)啟動(dòng)，具體步驟為：1) 發(fā)布者通過(guò)RPC請(qǐng)求向節(jié)點(diǎn)管理器注冊(cè)發(fā)布者信息，包括主題名topic1和RPC地址addr1，并將這些信息存儲(chǔ)到注冊(cè)列表中。2) 訂閱者向節(jié)點(diǎn)管理器訂閱主題topic1。3) 節(jié)點(diǎn)管理器根據(jù)訂閱者所需的主題topic1，在注冊(cè)列表中進(jìn)行查找。若匹配成功，節(jié)點(diǎn)管理器向訂閱者傳遞發(fā)布者的RPC地址addr1。4) 訂閱者聯(lián)系發(fā)布者獲取主題連接請(qǐng)求。5) 在收到訂閱者的連接請(qǐng)求后，發(fā)布者繼續(xù)通過(guò)RPC請(qǐng)求向訂閱者確認(rèn)連接信息，包括發(fā)布主題的TCP地址addr2。6) 訂閱者接收到確認(rèn)消息后，通過(guò)TCP請(qǐng)求連接到發(fā)布者地址addr2。7) 二者成功建立TCP連接，訂閱者開始接收發(fā)布者發(fā)出的消息數(shù)據(jù)。

圖1 ROS通信過(guò)程

1.2 JavaMOP[11]

運(yùn)行時(shí)驗(yàn)證系統(tǒng)的結(jié)構(gòu)[12-13]如圖2所示，它由運(yùn)行的程序和監(jiān)控器組成。監(jiān)控器通過(guò)分析程序的多個(gè)執(zhí)行路徑，將它們轉(zhuǎn)換為相應(yīng)事件，并結(jié)合給定的屬性，驗(yàn)證系統(tǒng)行為是否滿足屬性，對(duì)運(yùn)行結(jié)果作出判定。

圖2 運(yùn)行時(shí)驗(yàn)證結(jié)構(gòu)

運(yùn)行時(shí)驗(yàn)證的目的是實(shí)時(shí)監(jiān)控系統(tǒng)行為,驗(yàn)證系統(tǒng)的正確性[2]。通常使用面向監(jiān)控的編程(Monitoring-oriented Programming，MOP)[14]技術(shù)，這是一種擴(kuò)展了運(yùn)行時(shí)驗(yàn)證技術(shù)的輕量級(jí)形式化方法。MOP將屬性編織到原始系統(tǒng)中，并根據(jù)指定的屬性自動(dòng)生成監(jiān)控器。監(jiān)控器監(jiān)視程序在運(yùn)行期間的行為，當(dāng)違反規(guī)范時(shí)將觸發(fā)用戶定義的操作。JavaMOP[10，15-16]是一個(gè)針對(duì)Java的監(jiān)控編程開發(fā)工具，具有可插拔性和靈活性。JavaMOP規(guī)范主要包括變量(var)、事件(event)、屬性(property)和處理程序(handler)。

1) 變量。變量指的是待監(jiān)控的程序變量。

2) 事件。事件是目標(biāo)程序執(zhí)行期間發(fā)生的操作。它對(duì)應(yīng)于監(jiān)控程序中被監(jiān)控變量的更新，或者被監(jiān)控方法的調(diào)用。事件的聲明遵循AspectJ語(yǔ)義，事件被編織到Java程序中,被用來(lái)檢查是否符合屬性規(guī)約。

3) 屬性。屬性包括邏輯類型和邏輯語(yǔ)義，JavaMOP插件支持多種邏輯類型，如FSM(有限狀態(tài)機(jī))、LTL(線性速度邏輯)、ERE(擴(kuò)展正則表達(dá)式)、CFG(上下文無(wú)關(guān)文法)等。系統(tǒng)安全屬性可以用時(shí)態(tài)邏輯表示，本文主要以LTL邏輯[17-18]語(yǔ)句進(jìn)行介紹。LTL語(yǔ)法由原子命題和運(yùn)算符組成，運(yùn)算符包括[]，[*]，<>，<*>，o，(*)，！，not，U，S，And，Xor，Or，=>(蘊(yùn)含)[19]。T=t1,t2，…，ti,…，tn是一組原子命題，LTL語(yǔ)法及時(shí)態(tài)運(yùn)算符解釋如下：

· []μ:μ在所有的時(shí)間內(nèi)都是成立的。

· [*]μ:μ在過(guò)去的時(shí)間內(nèi)都是成立的。

· (*)μ:μ在之前的時(shí)間是成立的。

· <>μ:μ在將來(lái)的某個(gè)時(shí)間點(diǎn)成立。

· <*>μ:μ在過(guò)去的某個(gè)時(shí)間點(diǎn)成立

· oμ:μ在下一個(gè)時(shí)間點(diǎn)成立。

· μSv：自從μ成立的時(shí)間點(diǎn)起，v在過(guò)去的某個(gè)時(shí)刻已經(jīng)成立了。

· μUv：v在未來(lái)的某個(gè)時(shí)間點(diǎn)成立，μ在v成立之前已經(jīng)成立了。

4) 處理程序：處理程序由任意的Java代碼組成，用戶可以自定義操作，該操作可以是記錄異?；蛐畔⒏娜魏未a。以@fail、@violation或@validation開頭,分別代表自動(dòng)機(jī)的不確定、違背和驗(yàn)證三種狀態(tài)。

2 ROS-Monitor運(yùn)行時(shí)驗(yàn)證框架

ROS-Monitor是一個(gè)針對(duì)機(jī)器人操作系統(tǒng)的運(yùn)行時(shí)驗(yàn)證框架。如圖3所示，我們?cè)O(shè)計(jì)了一個(gè)能夠監(jiān)控所有節(jié)點(diǎn)活動(dòng)和節(jié)點(diǎn)消息的監(jiān)控中心節(jié)點(diǎn)，并將所有的待監(jiān)控信息存放到事件消息中樞。同時(shí)設(shè)計(jì)了一個(gè)代碼生成器，可以根據(jù)自定義場(chǎng)景描述自動(dòng)生成特定的監(jiān)控器。最后通過(guò)運(yùn)行監(jiān)控器，驗(yàn)證系統(tǒng)的安全屬性，若系統(tǒng)行為違反安全屬性邏輯，則發(fā)出違背警告。

圖3 ROS-Monitor框架

2.1 監(jiān)控中心節(jié)點(diǎn)

ROS主題通信機(jī)制詳見1.1節(jié)，節(jié)點(diǎn)管理器默認(rèn)啟動(dòng)在11311端口，系統(tǒng)各節(jié)點(diǎn)連接到該端口進(jìn)行主題發(fā)布等相關(guān)操作，節(jié)點(diǎn)管理器記錄各節(jié)點(diǎn)發(fā)布和訂閱的信息。為了獲取節(jié)點(diǎn)的所有信息，我們根據(jù)ROS的XML/RPC的通信協(xié)議，設(shè)計(jì)了一個(gè)支持節(jié)點(diǎn)注冊(cè)、主題發(fā)布訂閱等功能的監(jiān)控中心節(jié)點(diǎn)，可將其理解為節(jié)點(diǎn)管理器的代理。本框架將節(jié)點(diǎn)管理器啟動(dòng)在11111端口，監(jiān)控中心節(jié)點(diǎn)啟動(dòng)在11311端口。監(jiān)控中心節(jié)點(diǎn)一方面與節(jié)點(diǎn)管理器進(jìn)行通信，另一方面與系統(tǒng)各功能節(jié)點(diǎn)進(jìn)行通信，因此可以獲取ROS系統(tǒng)中所有待監(jiān)控的信息。

監(jiān)控中心節(jié)點(diǎn)需要監(jiān)控節(jié)點(diǎn)活動(dòng)和節(jié)點(diǎn)消息兩種事件類型，并把所有的數(shù)據(jù)存放到事件消息中樞。其中節(jié)點(diǎn)活動(dòng)類型是指在ROS系統(tǒng)中所有節(jié)點(diǎn)的活動(dòng)數(shù)據(jù)，包括節(jié)點(diǎn)的啟動(dòng)、發(fā)布主題、訂閱主題等事件。節(jié)點(diǎn)消息類型是指系統(tǒng)中各個(gè)節(jié)點(diǎn)之間傳遞的主題消息。

2.2 事件消息中樞

ROS程序主要由C++編寫，而JavaMOP是監(jiān)控Java程序的一種運(yùn)行時(shí)驗(yàn)證技術(shù)。為了能夠更好地利用JavaMOP技術(shù)，本系統(tǒng)設(shè)計(jì)了一個(gè)用于信息傳輸?shù)闹虚g件——事件消息中樞，它包括C++服務(wù)端和Java客戶端兩個(gè)部分。客戶端和服務(wù)端采用請(qǐng)求和應(yīng)答的方式進(jìn)行通信，服務(wù)端將待監(jiān)控的信息存放到一個(gè)緩沖消息隊(duì)列，客戶端主動(dòng)發(fā)起請(qǐng)求獲取服務(wù)端隊(duì)列中的數(shù)據(jù)。為了方便數(shù)據(jù)傳輸和解析，我們使用json字符串的方法將數(shù)據(jù)轉(zhuǎn)換成字節(jié)流。json是一種輕量級(jí)的數(shù)據(jù)交換格式，方法簡(jiǎn)單靈活，又具有表達(dá)多層次復(fù)雜內(nèi)容的能力。

針對(duì)節(jié)點(diǎn)消息類型，主題消息的內(nèi)容是一個(gè)結(jié)構(gòu)體數(shù)據(jù)。例如控制小車運(yùn)動(dòng)的“/cmd_vel”消息對(duì)應(yīng)的結(jié)構(gòu)數(shù)據(jù)是“geometry_msgs/Twist”，該結(jié)構(gòu)體“Twist.msg”包含3維浮點(diǎn)數(shù):“Vector3 linear(x,y,z)”和“Vector3 angular(x,y,z)”。其中線速度表示為“msg.linear.x”，角速度表示為“msg.angular.z”。為了方便使用，將其轉(zhuǎn)化成json字符串，如一個(gè)具體的消息數(shù)據(jù)為“[1,0,0][0,0,2]”則轉(zhuǎn)化后的json字符串為:“message”:{“cmd_vel”:{“x”:1,”y”:0,”z”:0},”angular”:{“x”:0,”y”:0,”z”:2}}}

針對(duì)節(jié)點(diǎn)活動(dòng)類型，包括節(jié)點(diǎn)注冊(cè)與注銷、主題發(fā)布與訂閱、消息發(fā)送與接收，具體字段和含義如表1所示。該類型數(shù)據(jù)同樣通過(guò)json字符串的方法進(jìn)行傳輸，如下所示：

表1 節(jié)點(diǎn)活動(dòng)類型

節(jié)點(diǎn)注冊(cè)：

{“node_event”:{“node”:“car”,“type”:“register”}}

發(fā)布主題：

{“node_event”:{“node”:“car”,“type”:“publish”,“topic”:“cmd_vel”}}

訂閱主題：

{“node_event”:{“node:car”,“type”:“subscribe”,“topic”:“cmd_vel”}}

2.3 自定義場(chǎng)景描述

一個(gè)正在運(yùn)行的ROS系統(tǒng)會(huì)產(chǎn)生許多節(jié)點(diǎn)活動(dòng)和節(jié)點(diǎn)消息數(shù)據(jù)，但是并非所有數(shù)據(jù)都需要監(jiān)控，僅需要關(guān)注與系統(tǒng)安全相關(guān)的部分。ROS中的待監(jiān)控?cái)?shù)據(jù)本身具有結(jié)構(gòu)化，我們通過(guò)一種形式化描述的方法更加方便地表達(dá)要監(jiān)控的數(shù)據(jù)。因此，本系統(tǒng)設(shè)計(jì)了一個(gè)代碼生成工具，可以根據(jù)自定義場(chǎng)景描述文件自動(dòng)生成特定的監(jiān)控器，包括Java代碼和Mop代碼。

表2是自定義場(chǎng)景描述字段和格式內(nèi)容說(shuō)明?！癝ource”字段指定監(jiān)控內(nèi)容的來(lái)源，它包括節(jié)點(diǎn)活動(dòng)或節(jié)點(diǎn)消息類型的數(shù)據(jù)，格式為“主題：主題名，或者節(jié)點(diǎn)：節(jié)點(diǎn)名”?！癡ar”表示要監(jiān)視消息中的變量，格式為“變量?jī)?nèi)容：消息結(jié)構(gòu)體值”?！癊vent”字段是節(jié)點(diǎn)活動(dòng)事件或節(jié)點(diǎn)消息變量監(jiān)控事件，格式為觸發(fā)函數(shù)的事件條件語(yǔ)句，它將與“Property”字段中的邏輯語(yǔ)句組合在一起形成屬性邏輯語(yǔ)義?！癙roperty”字段是一個(gè)屬性表達(dá)式，格式為“邏輯類型：邏輯語(yǔ)義”?！癡iolation”為違背字段，內(nèi)容為違背時(shí)的錯(cuò)誤執(zhí)行代碼段，如果該屬性被違反，將根據(jù)“Violation”字段后面的代碼內(nèi)容進(jìn)行打印警告。

表2 自定義場(chǎng)景描述說(shuō)明

2.4 監(jiān)控代碼生成機(jī)制

監(jiān)控器的代碼生成機(jī)制如圖4所示。代碼生成器能依次解析自定義場(chǎng)景描述的“Source”、“Var”、“Event”和“Property”字段內(nèi)容，計(jì)算出這幾個(gè)字段的內(nèi)部依賴關(guān)系，生成若干個(gè)代碼段。并將生成的代碼填充到預(yù)先準(zhǔn)備好的代碼模板中，最終生成完整的Java代碼和Mop代碼文件。其中生成的Java代碼包含一個(gè)TCP客戶端，該客戶端通過(guò)連接事件消息中樞獲取待監(jiān)控的數(shù)據(jù)。我們使用shell腳本在Ubuntu系統(tǒng)上編譯代碼，通過(guò)執(zhí)行javac等指令把Java代碼編譯成可執(zhí)行文件，通過(guò)javamop等指令把Mop文件編織成JavaMOP代理。

圖4 自動(dòng)代碼生成的主要流程

下面展示了一個(gè)生成的簡(jiǎn)單的“monitor.mop”文件，其中“RESET”是一個(gè)特殊表達(dá)式，可以將監(jiān)控器重置為初始狀態(tài)。

monitor()

event exceed_speed after():

call(**.exceed_speed())

ltl :[]!(exceed_speed)

@violation {System.out. println(“warning from mop”);RESET;}

2.5 界面設(shè)計(jì)

我們?cè)赨buntu14.04上成功地實(shí)現(xiàn)了ROS-Monitor框架。為了讓系統(tǒng)易操作和使用，提供了一個(gè)用戶界面，如圖5所示，用戶可以設(shè)置“Source”、“Var”、“Event”和“Property”字段內(nèi)容。當(dāng)用戶點(diǎn)擊“Generator”按鈕時(shí)，工具將根據(jù)自定義場(chǎng)景描述，自動(dòng)生成Java代碼和Mop代碼并編譯到JavaMOP代理中。當(dāng)用戶單擊“Reset”按鈕時(shí)，輸入內(nèi)容將被清除，如果監(jiān)控器正在運(yùn)行，它將被強(qiáng)制停止監(jiān)控。當(dāng)用戶點(diǎn)擊“Monitor”按鈕后，系統(tǒng)會(huì)結(jié)合場(chǎng)景描述內(nèi)容，監(jiān)控正在運(yùn)行ROS的系統(tǒng)。如果系統(tǒng)行為違背安全屬性，警告日志將被打印在“Monitor Result”文本框內(nèi)。

圖5 用戶界面

3 安全策略和實(shí)驗(yàn)

本節(jié)通過(guò)一個(gè)簡(jiǎn)單示例和一個(gè)綜合實(shí)驗(yàn)來(lái)介紹ROS-Monitor框架的使用。用戶可根據(jù)具體的需求，通過(guò)自定義場(chǎng)景描述生成特定的監(jiān)控器，即可方便地監(jiān)控系統(tǒng)行為。

3.1 簡(jiǎn)單示例

攻擊者可以通過(guò)在TCP/IP層構(gòu)造虛假請(qǐng)求包來(lái)偽造ROS節(jié)點(diǎn)。例如在節(jié)點(diǎn)注冊(cè)之前進(jìn)行發(fā)布或訂閱主題，該操作不符合主題發(fā)布的正常運(yùn)行順序，會(huì)帶來(lái)潛在威脅。因此必須ROS系統(tǒng)中節(jié)點(diǎn)在發(fā)布主題之前，確保該節(jié)點(diǎn)已經(jīng)注冊(cè)。假設(shè)系統(tǒng)發(fā)布節(jié)點(diǎn)為“talker”，則自定義場(chǎng)景描述為：

Source:

node: talker

Var: None

Event:

node_start: talker.register

node_publish: talker.publish

Property:

ltl:[]node_publish=>(*)node_start

violation:

System.out.println(“Suspicious Nodes”);

此示例對(duì)“talker”節(jié)點(diǎn)的注冊(cè)和發(fā)布進(jìn)行安全監(jiān)控。由于操作不涉及變量，“Var”字段為空。當(dāng)觸發(fā)“talker”節(jié)點(diǎn)注冊(cè)活動(dòng)時(shí)，激活“node_start”事件；觸發(fā)“talker”節(jié)點(diǎn)的發(fā)布主題時(shí)，激活“node_publish”事件。為了保證系統(tǒng)始終處于安全狀態(tài)，則必須保證在節(jié)點(diǎn)發(fā)布主題之前先注冊(cè)該節(jié)點(diǎn)，即在激活“node_pulish”事件之前先激活“node_start”事件，LTL語(yǔ)句為“[]node_publish=>(*)node_start”。若系統(tǒng)行為違背該安全屬性，則打印出“Suspicious Nodes”警告信息。

圖6顯示了節(jié)點(diǎn)發(fā)布的有限狀態(tài)機(jī)的轉(zhuǎn)化過(guò)程。其中“ST”指的是系統(tǒng)處于“start”狀態(tài)。“S”指的是系統(tǒng)處于“safety”狀態(tài)，“US”指的是系統(tǒng)處于“unsafety”狀態(tài)。當(dāng)“node_start”事件被激活時(shí)，系統(tǒng)從“ST”啟動(dòng)狀態(tài)遷移到“S”安全狀態(tài)。若之前未先激活“node_start”事件，而直接進(jìn)行“node_publish”事件操作，系統(tǒng)將遷移到“US”狀態(tài)并發(fā)出警告提示。

圖6 節(jié)點(diǎn)發(fā)布的有限狀態(tài)機(jī)

3.2 綜合實(shí)驗(yàn)

本節(jié)我們以一個(gè)綜合的案例介紹ROS-Monitor框架。無(wú)人駕駛汽車又稱為輪式移動(dòng)機(jī)器人，它通過(guò)車載傳感器感知周圍環(huán)境，獲取道路和障礙物信息來(lái)控制車輛的轉(zhuǎn)向和速度，從而使車輛能夠安全、可靠地在道路上行駛。

Gazebo[20]是ROS中的物理仿真環(huán)境，它是一款機(jī)器人的仿真軟件，基于ODE的物理引擎，可模擬機(jī)器人以及環(huán)境中很多物理特性。我們采用Gazebo建立無(wú)人駕駛小車模型，車身搭載激光雷達(dá)[21]。激光雷達(dá)數(shù)據(jù)量大、檢測(cè)距離遠(yuǎn)、精度高，可以獲取很多的三維坐標(biāo)信息。通過(guò)這些信息，我們可以檢測(cè)障礙物的方位，判斷它的大小、高度等。本實(shí)驗(yàn)基于Gazebo環(huán)境構(gòu)建了一個(gè)虛擬的駕駛道路場(chǎng)景，模擬小車通過(guò)十字路口的過(guò)程。期間進(jìn)行多次實(shí)驗(yàn)，讓小車分別以直行和轉(zhuǎn)彎的方式通過(guò)該路口。我們?cè)O(shè)計(jì)了小車在行駛過(guò)程中，必須保證的4個(gè)重要的安全屬性：

1) 節(jié)點(diǎn)必須遵循主題的發(fā)布訂閱規(guī)則，主題被訂閱之前，該主題已經(jīng)被發(fā)布了。即在“car”節(jié)點(diǎn)訂閱“cmd_vel”主題之前，“car_control”節(jié)點(diǎn)已經(jīng)發(fā)布了該主題。

2) 當(dāng)“car_control”節(jié)點(diǎn)發(fā)送消息時(shí)，該節(jié)點(diǎn)必須已發(fā)布主題，并且該節(jié)點(diǎn)處于未關(guān)閉狀態(tài)。

3) 當(dāng)汽車行駛到十字路口，不能超過(guò)十字路口限定速度16 km/h，否則發(fā)出超速警告。

4) 不允許“car”節(jié)點(diǎn)高速急轉(zhuǎn)彎通過(guò)十字路口。角度和速度分別不能同時(shí)超過(guò)50°和13 km/h。

根據(jù)上述安全屬性描述，我們?cè)O(shè)定自定義場(chǎng)景描述如下：

Source:

topic: cmd_vel

node: car_control, car

Var:

speed: cmd_vel.linear.x

angle:cmd_vel.angular.z

Event:

crtl_publish: car_control.publish

car_subsribe: car.subsribe

crtl_close: car-control.unregister

crtl_send: car_control.send

turn_speed: speed>13

turn_angle: angle>50

exceed_speed: speed>16

Property:

ltl:[]car_subsribe=>(*)crtl_publish

@violation: System.out.println(“violate publish subscribe“);

ltl:[]crtl_send=>(not crtl_close S crtl_publish)

@violation:System.out.println(“Suspicious Nodes”);

ltl:[]!exceed_speed

@violation:System.out.println(“exceed speed”);

ltl:[]!(turn_speed and turn_angle)

@violation: System.out.println(“Sharp turn at high speed”);

本實(shí)驗(yàn)運(yùn)行了2個(gè)小時(shí)，監(jiān)控結(jié)果參見表3。此實(shí)驗(yàn)共出現(xiàn)22條警告。其中，V1屬性違反次數(shù)為0，所有的節(jié)點(diǎn)都遵循發(fā)布/訂閱規(guī)則進(jìn)行通信。對(duì)于V2屬性，正常情況下較難發(fā)生，我們模擬了5次不合理的節(jié)點(diǎn)啟動(dòng)順序。關(guān)閉節(jié)點(diǎn)后，該節(jié)點(diǎn)發(fā)布主題消息，監(jiān)控器打印了5次違規(guī)警告。由于小車無(wú)法識(shí)別特殊路段的限速標(biāo)志，導(dǎo)致通過(guò)十字路口時(shí)，超過(guò)了我們?cè)O(shè)定的最大速度限制。因此汽車在V3屬性上顯示13條超速警告。對(duì)于V4屬性，有4個(gè)急轉(zhuǎn)彎警告是由于遇到突然出現(xiàn)的其他汽車時(shí)沒(méi)有及時(shí)進(jìn)行降速躲避。

表3 實(shí)驗(yàn)結(jié)果

通過(guò)實(shí)驗(yàn)分析，該框架可以全面監(jiān)視汽車每個(gè)節(jié)點(diǎn)的運(yùn)行狀態(tài)，在系統(tǒng)沒(méi)有違背安全屬性的情況下沒(méi)有發(fā)出告警信息，在系統(tǒng)違背安全屬性的情況能夠準(zhǔn)確打印告警，并且告警次數(shù)符合預(yù)期。以上實(shí)驗(yàn)驗(yàn)證了ROS-Monitor框架的可用性，保證了系統(tǒng)的正常安全通信。

4 結(jié) 語(yǔ)

針對(duì)ROS在節(jié)點(diǎn)活動(dòng)和消息通信方面存在的安全問(wèn)題，本文提出ROS-Monitor的運(yùn)行時(shí)驗(yàn)證框架。該工具可以將自定義描述場(chǎng)景生成特定的監(jiān)控器，包括自動(dòng)生成的Java代碼和Mop代碼，并支持LTL等時(shí)序邏輯對(duì)ROS進(jìn)行驗(yàn)證。在系統(tǒng)行為違反安全屬性時(shí)，打印相關(guān)警告信息。該框架適用于主題方式通信的ROS模型(支持Indigo版本)，該工具從場(chǎng)景描述到監(jiān)控結(jié)果的產(chǎn)生，實(shí)現(xiàn)了高度的簡(jiǎn)單化和自動(dòng)化，并通過(guò)實(shí)際的案例驗(yàn)證了該框架的實(shí)用性。ROS消息通信方式有主題和服務(wù)兩種類型，本框架僅對(duì)主題通信進(jìn)行安全驗(yàn)證，后續(xù)將在服務(wù)通信方面進(jìn)行相關(guān)研究。