Soter：使用“運(yùn)行保證” 編程安全機(jī)器人系統(tǒng)

編輯部編譯

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

用于安全運(yùn)動(dòng)規(guī)劃器的RTA

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

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

相關(guān)研究

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

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

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