本文關(guān)鍵詞： 混成系統(tǒng) 安全性驗證 障礙驗證生成 符號計算 達(dá)布多項式 雙線性矩陣不等式 抽象解釋 多項式優(yōu)化　出處：《華東師范大學(xué)》2017年博士論文　論文類型：學(xué)位論文

【摘要】：混成系統(tǒng)是一類復(fù)雜的動力系統(tǒng),其中既包含了連續(xù)演變行為又含有離散變遷行為,并且兩者又交織發(fā)生.連續(xù)演變狀態(tài)可用于描述各個獨立物理硬件的連續(xù)行為,離散變遷狀態(tài)可用于描述離散控制或不同模態(tài)切換行為.因此,使得混成系統(tǒng)能很好的應(yīng)用于嵌入式系統(tǒng)及其逐步發(fā)展衍生的信息物理融合系統(tǒng)(即CPS)的形式化分析與建模研究之中.隨著信息技術(shù)和制造工程的快速發(fā)展,嵌入式系統(tǒng)和CPS在眾多關(guān)系國計民生的安全攸關(guān)領(lǐng)域,如航空航天、智能交通、醫(yī)療衛(wèi)生等均有廣泛應(yīng)用.因而,結(jié)合數(shù)學(xué)與計算機方法研究混成系統(tǒng)安全問題已成為軟件工程領(lǐng)域的熱門而前沿的研究課題,具有重要的科學(xué)價值和實際意義.障礙函數(shù)生成方法作為混成系統(tǒng)安全驗證主流方法之一,由于避免了對混成系統(tǒng)狀態(tài)可達(dá)集計算的困難而廣受關(guān)注.這類方法關(guān)鍵問題在于兩方面,一方面,目前已有的障礙驗證條件過于保守;另一方面,障礙驗證條件求解模型計算復(fù)雜度高.對此,本文針對混成系統(tǒng)的障礙函數(shù)生成方法進(jìn)行深入研究,分別從以下三個角度:創(chuàng)造新的低約束障礙驗證條件、簡化障礙函數(shù)生成模型計算、復(fù)雜系統(tǒng)模型抽象方法進(jìn)一步降低障礙函數(shù)生成的計算復(fù)雜度進(jìn)行研究.本論文的主要成果及貢獻(xiàn)有以下幾點:·提出新的障礙驗證條件構(gòu)造.本文是基于采用Darboux多項式特殊性質(zhì)進(jìn)行構(gòu)造的一類障礙函數(shù),稱為Darboux型障礙函數(shù)生成.由于采用新的安全驗證條件構(gòu)造方式,因而能生成已有障礙驗證方法所不能生成的障礙函數(shù),通過實驗結(jié)果也可說明這點.另外,得益于Darboux型障礙驗證條件轉(zhuǎn)化而來的問題模型的特殊特點,本文提出一個LS-QP交叉投影的求解方式,能非常高效的計算Darboux型障礙函數(shù),實驗結(jié)果能證明本文提出的算法具有高效性.·提出一種新的基于BMI模型求解的障礙函數(shù)生成方法.首先利用SOS松弛方法將經(jīng)典的微分障礙函數(shù)驗證模型轉(zhuǎn)化為一類BMI約束求解模型.本文進(jìn)一步針對一般化BMI約束求解問題進(jìn)行研究,最終給出求解一般BMI約束問題的變向增廣拉格朗日迭代方法(Alternating Direction Augmented Lagrangian Method)的顯式表達(dá)式.將該結(jié)果用于障礙函數(shù)生成問題,并給出求解算法.與當(dāng)前主流軟件PENNON核心算法進(jìn)行比較,本文求解算法復(fù)雜度更低.·提出新的系統(tǒng)抽象方法.針對復(fù)雜的非線性混成系統(tǒng)模型本身進(jìn)行研究,提出線性抽象的構(gòu)造方法,避免了通過直接求解復(fù)雜的原系統(tǒng)障礙驗證所造成的高計算復(fù)雜度.將給定的非線性混成系統(tǒng)轉(zhuǎn)化成相應(yīng)的具有待定參數(shù)的線性抽象系統(tǒng),接著對抽象得到的線性系統(tǒng)運用量詞消去方法進(jìn)行線性障礙驗證生成,該線性混成系統(tǒng)的安全性同時保證了原系統(tǒng)的安全性.實驗證明,本文提出的基于線性抽象的障礙函數(shù)生成,能解決原本直接利用量詞消去不能解決的非線性系統(tǒng)安全問題.
[Abstract]:Hybrid systems are a class of complex dynamical systems, which contain both continuous evolution behavior and discrete transition behavior, and both occur intertwined. The continuous evolution state can be used to describe the continuous behavior of individual physical hardware. Discrete transition states can be used to describe discrete control or switching behavior in different modes. With the rapid development of information technology and manufacturing engineering, the hybrid system can be used in the formal analysis and modeling research of embedded system and its derived information physics fusion system (CPS). Embedded systems and CPS are widely used in many safety related fields, such as aerospace, intelligent transportation, medical and health, etc. It has become a hot and frontier research topic in the field of software engineering to study the security problems of hybrid systems by combining mathematics and computer methods. It has important scientific value and practical significance. The obstacle function generation method is one of the main methods for security verification of hybrid systems. Because of avoiding the difficulty of computing the state reachability set of hybrid systems, the key problem of this kind of method lies in two aspects: on the one hand, the existing obstacle verification conditions are too conservative; on the other hand, The computational complexity of the obstacle verification condition solving model is high. In this paper, the obstacle function generation method of the hybrid system is studied in depth, from the following three aspects: create a new low constraint obstacle verification condition, Simplify the calculation of obstacle function generation model, The abstract method of complex system model further reduces the computational complexity of obstacle function generation. The main achievements and contributions of this paper are as follows: 路A new obstacle verification condition is proposed. This paper is based on the use of Darboux. A class of barrier functions constructed by special properties of polynomials, It is called Darboux type obstacle function generation. Because of the new security verification condition construction method, it can generate obstacle function that existing obstacle verification method can not generate, which can also be explained by the experimental results. In addition, Due to the special characteristics of the problem model transformed by the Darboux obstacle verification condition, this paper proposes a solution method of LS-QP cross-projection, which can calculate the Darboux type obstacle function very efficiently. The experimental results show that the proposed algorithm is efficient. 路A new method of generating obstacle function based on BMI model is proposed. Firstly, the classical differential obstacle function verification model is transformed into a new one by using SOS relaxation method. In this paper, we further study the generalized BMI constraint solving problem. Finally, the explicit expression of the variable augmented Lagrangian iterative method for solving general BMI constraint problem is given. The result is used to generate the obstacle function. Compared with the current mainstream software PENNON core algorithm, the complexity of this algorithm is lower. A new system abstraction method is proposed, and the complex nonlinear hybrid system model itself is studied. A linear abstract construction method is proposed to avoid the high computational complexity caused by the direct solution of complex original system obstacles. The given nonlinear hybrid system is transformed into the corresponding linear abstract system with undetermined parameters. Then the linear system is verified and generated by quantifier elimination method. The security of the linear mixed system is also guaranteed. The obstacle function generation based on linear abstraction proposed in this paper can solve the security problems of nonlinear systems which can not be solved by using quantifiers directly.
【學(xué)位授予單位】：華東師范大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2017
【分類號】：O19

【相似文獻(xiàn)】

相關(guān)期刊論文 前7條

1 范雙南;;基于時間序列分析的混成系統(tǒng)可靠性評價方法[J];福建電腦;2011年03期

2 鄒進(jìn);林望;羅勇;曾振柄;;基于多面體包含的非線性混成系統(tǒng)可達(dá)性分析[J];計算機應(yīng)用;2013年05期

3 吳定豪,呂建;一種基于狀態(tài)空間的混成系統(tǒng)設(shè)計方法的理論基礎(chǔ)研究[J];南京大學(xué)學(xué)報(自然科學(xué)版);1999年05期

4 裴玉,李宣東,鄭國梁;LDPChecker——一個實時和混成系統(tǒng)模型檢驗工具[J];計算機研究與發(fā)展;2005年01期

5 林望;吳敏;楊爭峰;曾振柄;;基于符號數(shù)值混合計算的混成系統(tǒng)Lyapunov函數(shù)構(gòu)造[J];系統(tǒng)科學(xué)與數(shù)學(xué);2012年05期

6 陳祖希;徐中偉;霍偉偉;喻鋼;;基于Craig插值的線性混成系統(tǒng)符號化模型檢測[J];電子學(xué)報;2014年07期

7 ;[J];;年期

相關(guān)會議論文 前1條

1 任雁;田婕;孫輝;周永;;混成系統(tǒng)測試研究綜述[A];2011年通信與信息技術(shù)新進(jìn)展——第八屆中國通信學(xué)會學(xué)術(shù)年會論文集[C];2011年

相關(guān)博士學(xué)位論文 前7條

1 解定寶;混成系統(tǒng)有界模型檢驗優(yōu)化技術(shù)研究[D];南京大學(xué);2016年

2 王國濱;信息物理融合系統(tǒng)安全性驗證研究[D];華東師范大學(xué);2016年

3 曾霞;基于障礙函數(shù)生成的混成系統(tǒng)安全驗證研究[D];華東師范大學(xué);2017年

4 林望;基于符號數(shù)值混合計算的混成系統(tǒng)可信分析與驗證研究[D];華東師范大學(xué);2013年

5 趙劍;混成系統(tǒng)基于模型診斷的若干問題研究[D];吉林大學(xué);2012年

6 孔輝;基于歸納不變式的混成系統(tǒng)安全性驗證[D];清華大學(xué);2013年

7 李廣元;LTLC：面向?qū)崟r與混成系統(tǒng)的連續(xù)時序邏輯[D];中國科學(xué)院軟件研究所;2001年

相關(guān)碩士學(xué)位論文 前7條

1 楊陽;基于深度優(yōu)先搜索的混成系統(tǒng)有界可達(dá)性分析[D];南京大學(xué);2013年

2 蔣慧;基于遷移系統(tǒng)語義的線性混成系統(tǒng)分析[D];南京大學(xué);2013年

3 李國拯;基于組合形式規(guī)范的混成系統(tǒng)形式化驗證方法研究[D];南京航空航天大學(xué);2015年

4 鄒進(jìn);非線性混成系統(tǒng)的可達(dá)性分析[D];溫州大學(xué);2013年

5 李倩;基于形式化方法的混成系統(tǒng)安全性檢驗[D];華東師范大學(xué);2015年

6 錢宇清;Hybrid AADL：混成系統(tǒng)體系結(jié)構(gòu)分析與設(shè)計語言[D];華東師范大學(xué);2014年

7 錢磊;信息物理融合系統(tǒng)的形式化建模與討論[D];華東師范大學(xué);2013年

，

本文編號：1519328