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

有效

• 申請(qǐng)?zhí)枺?/td>: 202110352147.7
• 申請(qǐng)日: 2021-03-31
• 公開(kāi)（公告）號(hào): CN113031572B
• 公開(kāi)（公告）日: 2022-06-21
• 發(fā)明（設(shè)計(jì)）人: 陳鑫;沙猛;劉毅達(dá)
• 申請(qǐng)（專(zhuān)利權(quán)）人: 南京大學(xué)
• 主分類(lèi)號(hào): G05B23/02
• 分類(lèi)號(hào): G05B23/02
• 代理公司: 江蘇銀創(chuàng)律師事務(wù)所 32242
• 代理人: 孫計(jì)良

1.一種系統(tǒng)安全驗(yàn)證的方法，其特征在于，該方法涉及被控系統(tǒng)和連接并驅(qū)動(dòng)所述被控系統(tǒng)的控制器；其中，所述被控系統(tǒng)有N個(gè)狀態(tài)量，所述控制器獲取所述被控系統(tǒng)的N個(gè)狀態(tài)量，輸出M個(gè)驅(qū)動(dòng)量用以驅(qū)動(dòng)所述被控系統(tǒng)；其中，N個(gè)狀態(tài)量表示為：x＝{x₁，x₂，...，x_N}，M個(gè)驅(qū)動(dòng)量表示為：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中各個(gè)狀態(tài)量x_i的取值范圍：

不變式區(qū)域T：

非安全區(qū)域U：

初始區(qū)域I：

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

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

其中，f₁，f₂，...，f_N均為預(yù)先定義的被控系統(tǒng)關(guān)于N個(gè)狀態(tài)量和M個(gè)驅(qū)動(dòng)量的函數(shù)；

S2：構(gòu)建狀態(tài)向量x中各個(gè)狀態(tài)量的所述不變式區(qū)域T范圍內(nèi)的插值樣本得到插值樣本集；然后以所述插值樣本集中的各個(gè)插值樣本s_t通過(guò)所述控制器，得到所述控制器所輸出的各個(gè)驅(qū)動(dòng)量的插值驅(qū)動(dòng)量u_k(s_t)；再以所述各個(gè)插值樣本s_t和其對(duì)應(yīng)的插值驅(qū)動(dòng)量u_k(s_t)作為插值點(diǎn)對(duì)各個(gè)驅(qū)動(dòng)量的系數(shù)待定的多項(xiàng)式擬合函數(shù)進(jìn)行插值求解，得到所述系數(shù)待定的多項(xiàng)式擬合函數(shù)中的各個(gè)待定的系數(shù)的取值，從而得到各個(gè)驅(qū)動(dòng)量的多項(xiàng)式擬合函數(shù)P_k(x)；其中，s_t表示為第t個(gè)插值樣本；u_k(x)表示為所述控制器輸入狀態(tài)向量x后所輸出的第k個(gè)驅(qū)動(dòng)量；u_k(s_t)表示為第t個(gè)插值樣本輸入至所述控制器所輸出的第k個(gè)驅(qū)動(dòng)量；P_k(x)表示為所述控制器輸入狀態(tài)向量x后所輸出的第k個(gè)驅(qū)動(dòng)量的擬合量；其中，k∈[1..M]；

其中，所述系數(shù)待定的多項(xiàng)式擬合函數(shù)表示為：

P_k(x，c)＝∑_jc_jp_j(x)，k∈[1..M]；

其中，P_k(x，c)為所述控制器所輸出的第k個(gè)驅(qū)動(dòng)量的系數(shù)待定的多項(xiàng)式擬合函數(shù)，x表示為N個(gè)狀態(tài)量組成狀態(tài)向量；c_j為多項(xiàng)式擬合函數(shù)中第j個(gè)單項(xiàng)式p_j(x)的系數(shù)，c表示為待定的系數(shù)c_j所組成的待定系數(shù)向量；p_j(x)為次數(shù)不超過(guò)D1的關(guān)于狀態(tài)量x₁，x₂，...，x_N的單項(xiàng)式；其中D1預(yù)先設(shè)定；

S3：通過(guò)構(gòu)建評(píng)估樣本集對(duì)所述控制器所輸出的驅(qū)動(dòng)量u_k(x)和擬合量P_k(x)進(jìn)行誤差評(píng)估，得到各個(gè)驅(qū)動(dòng)量u_k(x)和擬合量P_k(x)之間的誤差ε_k，從而得到誤差集合ε＝{ε₁，ε₂，...，ε_M}；其中，ε_k表示為第k個(gè)驅(qū)動(dòng)量和其擬合量之間的誤差；

S4：根據(jù)不變式區(qū)域T、非安全區(qū)域U、初始區(qū)域I和誤差集合ε構(gòu)建關(guān)于系數(shù)待定的柵欄函數(shù)B(x，z)＝∑_jz_jb_j(x)的SOS約束集，然后將所述SOS約束集輸入至SOS求解器進(jìn)行求解得到系數(shù)待定的柵欄函數(shù)B(x，z)中各個(gè)單項(xiàng)式的系數(shù)z₁，z₂，z₃，....，從而得到候補(bǔ)柵欄函數(shù)B(x)；其中，z_j為柵欄函數(shù)B(x，z)中第j個(gè)單項(xiàng)式b_j(x)的系數(shù)，z表示為待定的系數(shù)z_j所組成的待定系數(shù)向量；b_j(x)為次數(shù)不超過(guò)D2的關(guān)于狀態(tài)量x₁，x₂，...，x_N的單項(xiàng)式；其中D2預(yù)先設(shè)定；

若SOS求解器對(duì)所述SOS約束集求解后無(wú)解，則結(jié)束；

S5：通過(guò)SMT求解器驗(yàn)證候補(bǔ)柵欄函數(shù)B(x)是否滿足其安全條件：

其中，

S6：若所述SMT求解器驗(yàn)證不滿足其安全條件，則將誤差集合ε中的各個(gè)誤差ε_k擴(kuò)大，然后重復(fù)步驟S4至S6直到誤差ε_k超出預(yù)先設(shè)定的范圍或者SMT求解器驗(yàn)證其滿足安全條件；

其中，所述SOS約束集為：

F＝{sos(σ₁(x))，sos(σ₂(x))，...，sos(σ_N(x))，sos(φ₁(x))，sos(φ₂(x))，...，sos(φ_N(x))，sos(μ₁(x))，sos(μ₂(x))，...，sos(μ_N(x))，sos(γ₁(x，r))，sos(γ₂(x，r))，...，sos(γ_M(x，r))，sos(B_Init(x，z))，sos(B_Inv(x，z，r))，sos(B_Unsafe(x，z))}；

其中，

其中，σ₁(x)，σ₂(x)，...，σ_N(x)，λ(x)，φ₁(x)，φ₂(x)，...，φ_N(x)，μ₁(x)，μ₂(x)，...，μ_N(x)均為關(guān)于狀態(tài)量x₁，x₂，...，x_N的系數(shù)待定的次數(shù)不超過(guò)D2-2的多項(xiàng)式；γ₁(x，r)，...，γ_m(x，r)為關(guān)于狀態(tài)量x₁，x₂，...，x_N和變量r₁，r₂，...，r_M的系數(shù)待定的次數(shù)不超過(guò)D2-2的多項(xiàng)式；

其中，其中，r₁，r₂，...，r_M為根據(jù)誤差ε₁，ε₂，...，ε_M所引入的變量；

f_i(x₁，x₂，...，x_N，P₁(x)+r₁，P₂(x)+r₂，...，P_M(x)+r_M)為前述函數(shù)f₁，f₂，...，f_N中將驅(qū)動(dòng)量參數(shù)u_k，k∈[1..M]替換成相應(yīng)的擬合函數(shù)多項(xiàng)式和引入變量之和P_k(x)+r_k后的函數(shù)。