FM2018 Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning
（International Symposium on Formal Methods）

摘要

• 摘要
• Introduction
• Related work
• 基礎(chǔ)定義
• 具體算法
• 評估方法
• 具體實驗
• • 汽車模型
• 其他影響實驗的因素
• • log-sum-exp 的參數(shù)α
  • 關(guān)于執(zhí)行時間
• 總結(jié)

摘要

隨著軟件和分布式計算的迅速發(fā)展，信息物理系統(tǒng)（CPS）被廣泛應(yīng)用于許多領(lǐng)域，如智能電網(wǎng)，自動駕駛汽車等。由于軟件和物理系統(tǒng)的復(fù)雜性，檢測CPS模型中的缺陷是困難的，傳統(tǒng)的系統(tǒng)驗證技術(shù)，如模型檢驗或定理證明，由于物理部件具有無窮多個狀態(tài)，很難應(yīng)用于CPS。為了有效地發(fā)現(xiàn)CPS模型中的缺陷，引入了以魯棒性為導(dǎo)向CPS模型性質(zhì)falsification方法。現(xiàn)有方法使用全局優(yōu)化技術(shù)來生成違反了CPS模型性質(zhì)的反例。然而，這些方法可能需要大量的模擬運行才能找到反例，往往超出了實際可行性。本文探索最先進(jìn)的深度強(qiáng)化學(xué)習(xí)（DRL）技術(shù)，以減少查找此類反例所需的模擬運行次數(shù)，并討論了具體方法和初步評估結(jié)果。
個人理解就是，如果做圖片和文本的對抗樣本的話，只需要很直觀的添加擾動就可以了，但是做系統(tǒng)的話，需要仿真出一系列的軌跡，就很麻煩，如果用RL的話，可以很自動化的仿真出這樣一條軌跡，并且這個軌跡還是能夠檢測系統(tǒng)缺陷的。

Introduction

傳統(tǒng)的用于保證CPS模型正確性的測試方法很難保證測試的高覆蓋率，因為狀態(tài)空間是無限的。可以用測試軟件系統(tǒng)的形式化方法諸如模型檢測和理論證明來縝密的驗證這個系統(tǒng)，但model check是不確定的，因為CPS的狀態(tài)空間是無限的；而理論證明又非常困難。 因此，引入了魯棒引導(dǎo)證偽[2]、[3]方法來有效地檢測CPS中的缺陷。
使用Metric Temporal Logic(MTL)和它的 Signal Temporal Logic (STL)常被用于表示CPS模型應(yīng)該滿足的（魯棒性）性質(zhì)，從而數(shù)字化度量一個CPS模型的魯棒性程度，然后通過在CPS模型的狀態(tài)空間中探索，確定魯棒性最小的系統(tǒng)參數(shù)作為測試的輸入?yún)?shù)。通過這種方式，魯棒性引導(dǎo)的證偽有助于生成缺陷引導(dǎo)系統(tǒng)參數(shù)（即反例），從而能夠更高效、更自動地檢測缺陷。盡管穩(wěn)健性引導(dǎo)證偽的不終止并不意味著沒有反例，這在一定程度上說明了CPS模型的正確性。
現(xiàn)有隨機(jī)全局優(yōu)化方法如模擬退火、交叉熵的方法來最小化時序邏輯公式的值。（loss函數(shù)？）為了測試CPS，我們需要生成一系列能夠使這些系統(tǒng)失敗的輸入。現(xiàn)有的魯棒性指導(dǎo)的證偽通常被表示為參數(shù)生成問題。 輸入分為幾個控制點，在這些點的輸入被視為系統(tǒng)參數(shù)。但是這些輸入和系統(tǒng)響應(yīng)之間的時序關(guān)系是被丟掉了的，并且代表輸入的控制點形成高維空間，在高維空間中進(jìn)行優(yōu)化是非常困難的。
在DRL在無功非線性系統(tǒng)（如游戲）上的成功應(yīng)用的啟發(fā)下，本文提出將偽造問題作為一個強(qiáng)化學(xué)習(xí)問題并進(jìn)行解釋，利用DRL的交互學(xué)習(xí)能力尋找反例。 我們關(guān)注的是reactive的CPS，即實時從環(huán)境中獲取輸入的CPS。 我們采用了兩種最先進(jìn)的強(qiáng)化學(xué)習(xí)(D RL)技術(shù)，即Asynchronous Advanced Actor Critic(A3C)和Double Deep-Q Network(D DQN)，來解決CPS上的魯棒性引導(dǎo)偽造問題。
本文的主要貢獻(xiàn)有：
（1）展示了怎樣將找到違反CPS模型魯棒性性質(zhì)的行為序列的問題轉(zhuǎn)化為深度強(qiáng)化學(xué)習(xí)（DRL）問題；
（2）實現(xiàn)提出的方法并進(jìn)行初步評估，結(jié)果證明利用DRL技術(shù)可以減少尋找CPS模型致錯輸入需要的模擬運行次數(shù)，進(jìn)而減少模擬運行的總時間。
（3）提出基于強(qiáng)化學(xué)習(xí)技術(shù)的CPS模型魯棒性性質(zhì)falsification問題的測試框架，為進(jìn)一步探索該問題提供了保障。

Related work

魯棒性指導(dǎo)的方法分為黑盒方法和灰盒方法。 黑盒方法可以進(jìn)一步分為將魯棒性偽造問題轉(zhuǎn)化為全局優(yōu)化問題的方法和基于統(tǒng)計建模的方法。 采用全局優(yōu)化技術(shù)的方法包括采用模擬退火的方法、 采用遺傳算法的方法、Tabu search（禁忌搜索）、梯度下降等。 基于統(tǒng)計建模的方法包括交叉熵法、高斯回歸。
在控制器合成領(lǐng)域也有采用強(qiáng)化學(xué)習(xí)(RL)來滿足MTL性質(zhì)的方法。 這項任務(wù)的挑戰(zhàn)之一是如何從給定的公式設(shè)計RL中的獎勵。 一種策略是探索基于自動機(jī)的獎勵塑造[31]、[32]、[33]。 這些方法將MTL公式轉(zhuǎn)換為相應(yīng)的自動機(jī)，并根據(jù)自動機(jī)的當(dāng)前狀態(tài)決定獎勵。 另一種方法使用MTL的健壯性。控制器生成方法是要將系統(tǒng)一直保持在安全的狀態(tài)中，但證偽方法是找出系統(tǒng)的漏洞，不同的目的對應(yīng)了不同的獎勵函數(shù)設(shè)置。

基礎(chǔ)定義

• 我們關(guān)注的是能夠?qū)崟r輸入并且輸出的系統(tǒng)，并且假設(shè)輸入和輸出是發(fā)生在一瞬間的離散的時刻。連續(xù)的系統(tǒng)可以通過采樣來適應(yīng)離散的系統(tǒng)。這個系統(tǒng)就是一個函數(shù)f ：X* -> Y X*是輸入的集合，Y是輸出。f(x${}_1$, . . . , x${}_i$) = y${}_{i+1}$ ，意思是連續(xù)輸入i次，輸出的結(jié)果記為y${}_{i+1}$ 。
• 定義 Dist(x, D) 是輸入集合X中的一個點x 到 X的閉合子集D的距離。inf是指下確界。相當(dāng)于min，但是不是min，最簡單的情況如果z是一個開區(qū)間的話，可能沒有最大最小值，但是是可以有上確界sup和下確界inf的。如果x屬于D的話，那么他的下確界是離開這個區(qū)域的最短距離，是個正值；如果x不屬于D那么他的下確界是到D這個區(qū)域的最小距離，但是這里取了負(fù)值，表示不在這個區(qū)域。（也就是說出了安全區(qū)域，就很差了，魯棒性就為負(fù)值。即使在安全區(qū)域里面，他離出安全區(qū)域越近他的魯棒性就越低）
  
• 然后。定義了魯棒性數(shù)值的衡量 degree[[φ]] (y,t) 表示輸出信號y在時間t對φ的魯棒性
• φ是一個MTL-formula，他的規(guī)則如下所示，直觀的說就是，y${}_n$這個狀態(tài)滿足p這個屬性。當(dāng)然還可以進(jìn)行一些與、或等邏輯判別。定義1：y是系統(tǒng)的輸出，n是表示經(jīng)歷了n個x的輸入，如t${}_n$,表示的這個時間瞬間。t = t${}_0$…t${}_n$…表示的是這個系統(tǒng)狀態(tài)的無限采樣的時間序列。 y=y${}_0$，y${}_1$，…，y${}_n$，…分別為時間瞬間的系統(tǒng)狀態(tài)。y, n |= φ 表示y${}_n$滿足φ這個屬性。
  
• 同時還引用其他文章中 未來可到達(dá) fr§ 的定義，表示未來確定p這個屬性是真值所需要的最小時間。如果fr§=0的話就表示，這屬性是"單純的過去依賴"屬性，意思就是過去的狀態(tài)已經(jīng)能夠滿足這個屬性了。他這里舉的例子的意思是，如果p已經(jīng)確定為真，fr§=0，要確定在之后的0~3秒里面p都是真，要第三秒才能知道；要確定從當(dāng)前時間之前的-3秒到0秒里面p是真在第0秒就能知道了(因為他fr§=0了嘛表示當(dāng)前已經(jīng)滿足了，所以最晚也是第0秒就能知道)
  
• 緊接著我們需要定義一個monitoring formula。因為我們希望關(guān)心的安全屬性不是一個單純的過去依賴，也就是說，不是一個只滿足某個瞬間的狀態(tài)，而是一定時間內(nèi)能滿足的， 這個monitoring formual φ${}_0$相當(dāng)于屬性φ的一個近似，而文中為了簡化問題，將φ${}_0$定義為 單純的過去依賴的，也就是可以立即判別的。

具體算法

• 文章使用了兩種強(qiáng)化學(xué)習(xí)算法 Asynchronous Advantage Actor-Critic (A3C) 和Double Deep Q Network (DDQN)。A3C主要就是將原本的DQN分成了兩部分，Actor學(xué)習(xí)動作和Critic學(xué)習(xí)值函數(shù)估值，兩個互相獨立的神經(jīng)網(wǎng)絡(luò)，但是Critic會影響Actor。DDQN主要是為了解決DQN的過估計問題，弄了兩個一模一樣的網(wǎng)絡(luò)，在學(xué)習(xí)估值的時候用max來做評估，在選擇輸出動作的時候用另一個沒有做過max 評估的權(quán)重集合來做動作，一定程度上降低了過估計的可能性，對動作選擇和動作估值進(jìn)行解耦，收斂更平滑。（文章只做了簡要介紹，沒有具體展開，感覺需要再寫一篇來專門學(xué)習(xí)這幾個算法才能徹底弄懂，因為本身也是原始DQN的優(yōu)化算法，所以暫時就默認(rèn)他們作為DL的作用）
• 給定安全屬性φ，以及它的monitoring formual φ${}_0$， 系統(tǒng)和主體，我們的目的是輸出一個x集合，使得執(zhí)行完x里面的動作后，系統(tǒng)的輸出是不符合安全屬性的。每次對系統(tǒng)進(jìn)行L步的仿真，如果最后結(jié)果里面有狀態(tài)是不安全的，那么就把這組輸入保存下來作為一個對抗樣本，否則就在保留主體記憶的情況下又從頭開始仿真學(xué)習(xí)。其中，仿真的步數(shù)L和進(jìn)行的輪數(shù)N是可以自主設(shè)定的參數(shù)。
• reward的定義如下，直觀的講就是對當(dāng)前輸出進(jìn)行評價，如果魯棒性越小，reward就越大。
  

評估方法

• 一共做了三個實驗的對比實驗（隨機(jī)均勻采樣）uniform random sampling (RAND), （交叉熵）Cross Entropy (CE) and （模擬退火)Simulated Annealing (SA)。將隨機(jī)采樣作為本次實驗的目標(biāo)基準(zhǔn)線，所有的實驗結(jié)果和它進(jìn)行比較之后的結(jié)果作為不同方法好壞的判斷標(biāo)準(zhǔn)。后面兩種方法不太了解emmmm應(yīng)該還需要繼續(xù)學(xué)習(xí)才能明白。
• 此外計算200輪中成功找到對抗樣本的比例和找到對抗樣本輪數(shù)的中位數(shù)。 使用中位數(shù)而不是平均數(shù)的原因是，偽造所需輪數(shù)的分布高度不正常，因此平均沒有意義。
• 但以上兩種方法不足以反應(yīng)結(jié)果的分布差異還采用了一個“相對效應(yīng)大小”度量方法，有兩個隨機(jī)數(shù)X和Y，為了比較他們兩個誰的范圍更大，就求X小于Y的概率：p如果小于0.5，說明X<Y小的概率很小，那么X大部分情況比Y大。
• 而我們這里想知道，在比較方法A和B的時候，A比B表現(xiàn)更好的頻率有多高，而平均值和中位數(shù)，只是在強(qiáng)有力的假設(shè)下間接的說明這個問題，是不夠直觀的。
  

具體實驗

• 作者們做了三個實驗，每個實驗工作量一個比一個龐大= =，這里只以第一個相對簡單的實驗介紹一下

汽車模型

• 如上圖所示，這個模型輸入是Throttle (節(jié)氣門？)向量 和 Brake（制動器）值。輸出五個參數(shù)包括速度等。然后根據(jù)屬性的復(fù)雜性定義了如下幾個等級的屬性（eg,φ${}_4$表示了系統(tǒng)續(xù)航力，φ${}_5$體現(xiàn)了系統(tǒng)的反應(yīng)能力等）：
  
• 對于兩個強(qiáng)化學(xué)習(xí)算法的實驗，還分別作了黑盒和白盒的測試，這里文章只提了一句話說，白盒是能觀察到完整的輸出y1~ y5，黑盒只能觀察到魯棒性結(jié)果。后面解釋了= =是指的強(qiáng)化學(xué)習(xí)算法中，每次仿真完系統(tǒng)，白盒會得到y(tǒng)1~y5的作為y${}_i$進(jìn)行學(xué)習(xí)即整個系統(tǒng)的狀態(tài)，但黑盒是使用的y${}_i$的魯棒性數(shù)值不能觀察到系統(tǒng)的整個狀態(tài)。下圖表示的是成功找到對抗樣本的比例：
  
• 下面這張是模型成功次數(shù)的中位數(shù)及其可視化。TABLE4和TABLE5是之前提到的“相對效應(yīng)大小”來比較兩種方法誰有更高的概率性能更優(yōu)。表中的值越小，就說明列方法比行方法更小，更集中->也就是說偽造成功的次數(shù)越低。（其實可視化的圖已經(jīng)很直觀了= =）
  
  

其他影響實驗的因素

log-sum-exp 的參數(shù)α

通過實驗得出，整體而言阿爾法不會對結(jié)果造成很大影響。

關(guān)于執(zhí)行時間

• 因為還要考慮不同方法使用的語言差異，環(huán)境差異等這里使用仿真次數(shù)作為單位來衡量執(zhí)行時間，因為執(zhí)行一步主要時間其實是在仿真上面的，迭代次數(shù)越少，總執(zhí)行時間就會越少。同時也評估了$\Delta$T執(zhí)行時間的影響，如果有影響的話小的$\Delta$T就會使學(xué)習(xí)的迭代次數(shù)增加那么，就也會更慢，但實驗證明并沒有大影響（除了$\phi$${}_5$，文章解釋說應(yīng)該是因為這個屬性只需要非常少的模擬次數(shù)，所以初始化開銷占了大部分執(zhí)行時間。沒太懂，感覺這里的意思是執(zhí)行時間還是真實的時間，只是計量單位用的仿真次數(shù)）。這樣也是為了盡量避免因為執(zhí)行環(huán)境和選取的編程語言帶來的差異。

總結(jié)

• 提出了一種生成信息物理系統(tǒng)（CPS）對抗樣本的強(qiáng)化學(xué)習(xí)方法
• 并且展示了如何將一個CPS對抗樣本生成問題轉(zhuǎn)化成強(qiáng)化學(xué)習(xí)問題
• 進(jìn)行了實驗對比了多種不同方法和RL方法的差異，并且使用“相對影響大小”的方法來進(jìn)行分析。并且找到了影響RL結(jié)果兩個因素：是否能觀察的整個系統(tǒng)的結(jié)果以及輸入結(jié)構(gòu)，另一個因素是偽造輸入中存在可學(xué)習(xí)的結(jié)構(gòu)。

總結(jié)

以上是生活随笔為你收集整理的【阅读笔记】Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning的全部內(nèi)容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯，歡迎將生活随笔推薦給好友。