[發(fā)明專利]一種系統(tǒng)安全驗證的方法和裝置

有效

• 申請?zhí)枺?/td>: 202110352147.7
• 申請日: 2021-03-31
• 公開（公告）號: CN113031572B
• 公開（公告）日: 2022-06-21
• 發(fā)明（設計）人: 陳鑫;沙猛;劉毅達
• 申請（專利權）人: 南京大學
• 主分類號: G05B23/02
• 分類號: G05B23/02
• 代理公司: 江蘇銀創(chuàng)律師事務所 32242
• 代理人: 孫計良

本發(fā)明公開了一種系統(tǒng)安全驗證的方法和裝置。該方法首先通過多項式插值方法對控制器進行多項式抽象，并估計兩者之間誤差上界，以此將控制器擬合成帶擾動的抽象多項式；然后通過利用SOS松弛求解得到被控系統(tǒng)的候補柵欄函數(shù)；最后采用SMT求解器候補柵欄函數(shù)是否滿足最終結果的正確性。相比于傳統(tǒng)的基于可達集的驗證方法，本發(fā)明能夠驗證無窮時間域上的安全性。此外，相比于數(shù)據驅動的柵欄函數(shù)生成算法，本發(fā)明所生成候補柵欄函數(shù)更為精確。

技術領域

本發(fā)明涉及系統(tǒng)可滿足性驗證。

背景技術

深度神經網絡控制器在很多安全攸關的領域得到了越來越廣泛的應用，如自動駕駛，無人機和飛機避障等，但它們的安全性和可靠性研究一直是比較欠缺的；近年來，這些系統(tǒng)的一些安全事故的發(fā)生更是引發(fā)了廣泛的安全需求。

已有的研究主要集中在可達集分析方法上，主要通過集合運算計算從初始化區(qū)域出發(fā)的系統(tǒng)軌跡的可達集或其過近似，并判斷是否與非安全區(qū)域有交集。這種方法只能驗證有限時間內的安全性，且隨著輸入維度的增大過近似的誤差會快速增大，導致可擴展性不足。

另一種研究方法是基于柵欄函數(shù)的思想，這種方法能夠驗證無窮時間上的安全性，但已有的工作主要是數(shù)據驅動的生成方法，缺少更加精準的生成方法。

發(fā)明內容

本發(fā)明所要解決的問題：對控制器所控制的系統(tǒng)進行安全性驗證。

為解決上述問題，本發(fā)明采用的方案如下：

根據本發(fā)明的一種系統(tǒng)安全驗證的方法，該方法涉及被控系統(tǒng)和連接并驅動所述被控系統(tǒng)的控制器；其中，所述被控系統(tǒng)有N個狀態(tài)量，所述控制器獲取所述被控系統(tǒng)的N個狀態(tài)量，輸出M個驅動量用以驅動所述被控系統(tǒng)；其中，N個狀態(tài)量表示為：x＝{x₁,x₂,…,x_N}，M個驅動量表示為：u＝{u₁,u₂,…,u_M}；其中，N≥1,M≥1；所述方法包括以下步驟：

S1：獲取所述被控系統(tǒng)的狀態(tài)量的不變式區(qū)域T、非安全區(qū)域U、初始區(qū)域I和常微分方程建模的系統(tǒng)行為；所述不變式區(qū)域T、非安全區(qū)域U、初始區(qū)域I定義了所述狀態(tài)向量x中各個狀態(tài)量x_i的取值范圍：

不變式區(qū)域T：

非安全區(qū)域U：

初始區(qū)域I：

其中，所述非安全區(qū)域U和初始區(qū)域I均在所述不變式區(qū)域T的范圍內，即滿足條件：

以及

所述常微分方程建模的系統(tǒng)行為表示為：

其中，f₁,f₂,…,f_N均為預先定義的被控系統(tǒng)關于N個狀態(tài)量和M個驅動量的函數(shù)；