編輯部編譯

如今，得益于技術(shù)的不斷進步和成熟，機器人系統(tǒng)的應(yīng)用越來越普遍，但人們對于機器人系統(tǒng)的高要求無形中也增加了系統(tǒng)的復(fù)雜度。然而，形式驗證和系統(tǒng)測試的進步速度與復(fù)雜度的增加速度并不成正比。那么，我們該如何確保機器人系統(tǒng)的安全性呢？最近，伯克利加州大學(xué)的Ankush Desai、Shromona Ghosh、Sanjit A. Seshia、Natarajan Shankar和Ashish Tiwari等研究人員針對這一問題進行研究，提出了運用“運行保證”技術(shù)來解決這一問題。

隨著技術(shù)的成熟，機器人系統(tǒng)在社會中發(fā)揮著越來越多的安全性、關(guān)鍵性作用，比如，交付系統(tǒng)、監(jiān)視系統(tǒng)，以及個人交通等。與此同時，這種對于自動化的追求趨勢也導(dǎo)致了系統(tǒng)復(fù)雜程度的不斷提高，包括高級數(shù)據(jù)驅(qū)動的機器學(xué)習組件的集成。然而，形式驗證（formal verification）和系統(tǒng)測試的進步尚未能夠跟上日益增加的復(fù)雜度。此外，機器人系統(tǒng)對第三方現(xiàn)成組件和機器學(xué)習技術(shù)的依賴性預(yù)計會增加，這將導(dǎo)致正在部署的系統(tǒng)的復(fù)雜性，與通過形式驗證獲得安全性和正確性認證的系統(tǒng)之間的差距越來越大。

彌合這一差距的一種方法是利用運行保證（run-time assurance，RTA）技術(shù)，其中，設(shè)計時的驗證結(jié)果可用于構(gòu)建一個系統(tǒng)，該系統(tǒng)在運行時監(jiān)控自身及其環(huán)境，并切換到可證明安全性的運行模式，有可能性能較低，且會犧牲某些非關(guān)鍵性的目標。運行保證（RTA）框架的一個突出例子是單純形架構(gòu)（Simplex Architecture），已被用于構(gòu)建具有一定正確性的安全關(guān)鍵航空電子設(shè)備、機器人和網(wǎng)絡(luò)物理系統(tǒng)。Simplex架構(gòu)將一個未經(jīng)認證的高級控制器（AC）與一個經(jīng)過認證的正確安全控制器（SC），以及決策模塊（DM）相結(jié)合，其中DM的作用是在AC和SC之間切換，以使整個系統(tǒng)保持安全。然而，RTA之前的大多數(shù)應(yīng)用，在設(shè)計用于這種系統(tǒng)的定時和通信行為時，不提供高級語言支持，用于以一種模塊化方式構(gòu)造可證明安全性的RTA系統(tǒng)。以往的技術(shù)要么將RTA應(yīng)用于系統(tǒng)中的單個不可信組件，要么將大型單片系統(tǒng)包裝到Simplex的單一實例中，而這使得相應(yīng)的SC和DM的設(shè)計和驗證變得困難或不可行。Schierman等人對如何在無人駕駛飛機系統(tǒng)的軟件堆棧的不同級別上使用RTA框架進行了研究。在最近的一項研究中，Schierman等人提出了一種基于組件的單純形架構(gòu)（CBSA），它將假設(shè)保證合同（assume-guarantee contracts）與RTA相結(jié)合，以確?；诮M件的網(wǎng)絡(luò)物理系統(tǒng)運行時的安全性。然而，為了便于構(gòu)建RTA系統(tǒng)，需要一種通用編程框架，用于構(gòu)建具有運行保證的、可證明安全性的機器人軟件系統(tǒng)，且該系統(tǒng)還考慮諸如定時和通信的實現(xiàn)方面。

在本文中，我們試圖使用Soter來解決這一需求，Soter是一個使用運行保證構(gòu)建安全機器人系統(tǒng)的編程框架。Soter程序是周期性過程的集合，稱為節(jié)點，它使用一個“發(fā)布—訂閱”的通信模型進行交互。Soter中的RTA模塊由一個高級控制器節(jié)點、一個安全控制器節(jié)點和一個安全規(guī)范組成，如果模塊格式良好，則框架提供一個系統(tǒng)滿足安全規(guī)范的保證。Soter使得程序員能夠以聲明的方式構(gòu)建一個具有指定時序行為的RTA模塊，將可證明安全性的操作與安全時使用AC的特征相結(jié)合，以實現(xiàn)良好的性能。我們的評估表明，Soter能夠有效地實現(xiàn)這種安全性和性能的融合。

Soter采用了用于將整個RTA系統(tǒng)的設(shè)計和驗證分解為單個RTA模塊的結(jié)構(gòu)，同時保證了整個復(fù)合系統(tǒng)的安全性。Soter包括一個編譯器，它能夠生成實現(xiàn)切換邏輯的DM節(jié)點，并生成C代碼，以便在諸如機器人操作系統(tǒng)（ROS）和MavLink等常見的機器人軟件平臺上執(zhí)行。

我們通過構(gòu)建一個安全的自主無人機監(jiān)控系統(tǒng)對Soter框架的有效性進行評估。我們展示了Soter可用于構(gòu)建一個由第三方不可信組件和復(fù)雜機器學(xué)習模塊組成的復(fù)雜機器人軟件堆棧，并且仍然能夠提供系統(tǒng)范圍內(nèi)的正確性保證。生成的機器人軟件代碼已經(jīng)在實際無人機平臺（3DR無人機）和模擬（使用ROS/Gazeb和OpenAI Gym）上進行了測試。我們的測試結(jié)果表明，使用Soter構(gòu)建的受RTA保護的軟件堆棧，可以在使用不安全的第三方控制器的時候，以及在高級控制器中使用故障注入引入bug的時候，確保無人機的安全性。

總而言之，我們的論文做出了以下新穎的貢獻：

1.一個基于Simplex的運行保證系統(tǒng)的編程框架，為安全機器人系統(tǒng)的模塊化設(shè)計提供了語言原語；

2.一個基于可達集計算的理論形式，使得系統(tǒng)能夠保持可靠安全性，同時保持安全和高級控制器之間的平滑切換行為；

3在模擬和實際無人機平臺上的實驗結(jié)果表明，在存在不可信或未經(jīng)驗證的組件的情況下，Soter是如何用于保證系統(tǒng)的正確性的。

運行保證的體系結(jié)構(gòu)

圖1顯示了由三個子組件組成的RTA架構(gòu)（類似于Simplex）：（1）在正常操作條件下控制機器人的高級控制器（AC），并且旨在實現(xiàn)涉及特定度量（例如，成本和時間）的高性能。AC針對性能進行了優(yōu)化，并且沒有附帶安全證書。（2）安全控制器（SC），可以進行預(yù)先認證，以使得機器人保持在工廠/機器人的安全操作區(qū)域內(nèi)運行。（3）經(jīng)過預(yù)先認證（或自動合成為正確）的決策模塊（DM），以定期監(jiān)視工廠的狀態(tài)，并確定何時從AC切換到SC，以確保系統(tǒng)保持在安全區(qū)域內(nèi)。

當AC控制系統(tǒng)時，DM每隔Δ周期對系統(tǒng)狀態(tài)進行監(jiān)視（采樣），以檢查系統(tǒng)是否能夠在時間Δ內(nèi)違反預(yù)期的安全規(guī)范（φ）。如果是，則DM切換控制到SC。我們將DM從AC切換到SC的條件作為切換條件。

案例研究：無人機監(jiān)控系統(tǒng)

在本文中，我們考慮建立一個監(jiān)視系統(tǒng)，其中，自主無人機必須安全地在城市中巡邏。圖2a（頂部）顯示了來自Gazebo模擬器的工作空間快照。圖2a（底部）顯示了工作空間的障礙物圖，所有障礙物（房屋、汽車等）都是靜態(tài)的。

圖2b顯示了無人機監(jiān)控系統(tǒng)的軟件堆棧。應(yīng)用層實現(xiàn)監(jiān)視協(xié)議，該協(xié)議確保應(yīng)用特定屬性（φapp），例如，必須經(jīng)常性地訪問所有監(jiān)視點。軟件堆棧的通用組件包括運動規(guī)劃器和運動原語。該應(yīng)用程序為無人機生成下一個目標位置。運動規(guī)劃器對運動計劃進行計算，該運動計劃是從當前位置到目標位置的一系列路標點。圖2a（底部）中的w1…w6，表示由運動規(guī)劃器生成的運動計劃，虛線表示無人機的參考軌跡。在接收下一個路標點上的運動原語模塊生成所需的低級控制，以密切跟蹤參考軌跡。圖2a（底部）中的軌跡表示無人機的實際軌跡，由于潛在的動力學(xué)、干擾等因素，它偏離了參考軌跡。

用于安全運動規(guī)劃器的RTA

我們使用的是OMPL，這是一個第三方運動規(guī)劃庫，它實現(xiàn)了許多最先進的基于采樣的運動規(guī)劃算法。我們使用來自O(shè)MPL的RRT算法為我們的監(jiān)控應(yīng)用程序?qū)崿F(xiàn)了運動規(guī)劃器。

總而言之，我們使用格式良好的RTA模塊理論構(gòu)建了三個RTA模塊：運動原語、電池安全性和運動規(guī)劃器。受RTA保護的軟件堆棧（圖2c）是三個模塊的組合，在研究中，很多受RTA保護的軟件堆棧中的軟件進行了循環(huán)仿真。我們還將生成的代碼在真正的無人機上進行了部署，以進行類似的實驗。

相關(guān)研究

在這篇文章中，我們對此次的研究進行了詳細的概述?？梢哉f，單純形架構(gòu)除了廣泛用于航空電子和機器人領(lǐng)域外，在其他領(lǐng)域也有著廣泛的應(yīng)用。D.Phan、J.Yang等人提出了基于組件的單純形架構(gòu)和A-G合同，用于自動確定開關(guān)邏輯并在需要時執(zhí)行協(xié)調(diào)切換。在本文中，我們使用這些原理在Matlab中為QuickBot設(shè)計原型軟件堆棧。從文中，我們可以獲得一些靈感，并從以下兩個問題的解決中為以后的研究奠定了基礎(chǔ)：（1）我們提出了一個用于組合性構(gòu)建系統(tǒng)的編程框架，以便整個系統(tǒng)的安全問題可以分解為由單一模塊保證的RTA不變量。（2）我們使用該框架來構(gòu)建安全的無人機任務(wù)。一個重要的區(qū)別是，我們使用φsafer來確保系統(tǒng)的高性能行為。在《用于網(wǎng)絡(luò)物理系統(tǒng)的沙箱控制器》中，作者將Simplex方法應(yīng)用于沙箱網(wǎng)絡(luò)物理系統(tǒng)，并提出了一種基于自動可達性的方法來推斷切換條件。

我們將一個通用運行保證架構(gòu)進行了形式化，并在移動機器人系統(tǒng)的編程框架中實現(xiàn)它。安全關(guān)鍵系統(tǒng)的安全控制是一個非?；钴S的研究領(lǐng)域。可達性（Reachability）分析經(jīng)常用于研究控制系統(tǒng)的安全性。在正常條件下使用高級控制器（AC）的想法得到了研究人員的關(guān)注，在邊界處，使用最佳安全控制（SC）來保持安全性已經(jīng)用于在現(xiàn)實世界中操作四旋翼飛行器。我們可以使用這些方法來設(shè)計SC，并且在某些情況下，可以使用我們的框架來構(gòu)建那些已經(jīng)使用切換邏輯的系統(tǒng)。

運行驗證已應(yīng)用于機器人中，其中，監(jiān)視器用于檢查路徑規(guī)劃器和任務(wù)執(zhí)行的狀態(tài)。在本文中，我們實現(xiàn)了一個基于運行保證的編程框架，該框架支持復(fù)原以確保在現(xiàn)實世界中安全執(zhí)行機器人系統(tǒng)。最近，ModelPlex將CPS模型的離線驗證與系統(tǒng)執(zhí)行的運行驗證相結(jié)合，以便通過構(gòu)造運行監(jiān)視器來構(gòu)建正確的模型，從而為運行時的CPS執(zhí)行提供正確的保證。雖然ModelPlex的目標與我們的RTA框架相似，但它在兩個方面有所不同：（1）它依賴于可用模型的完整知識（或在我們的情況下是Nac）；（2）雖然它將切換條件綜合到Nsc，但它沒有提供Nac可以接管控制的條件，即它們不構(gòu)建φsafer。未來，對于這項研究，我們還會繼續(xù)探索。