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

【摘要】：混成系統(tǒng)是一類復(fù)雜的動(dòng)力系統(tǒng),其中既包含了連續(xù)演變行為又含有離散變遷行為,并且兩者又交織發(fā)生.連續(xù)演變狀態(tài)可用于描述各個(gè)獨(dú)立物理硬件的連續(xù)行為,離散變遷狀態(tài)可用于描述離散控制或不同模態(tài)切換行為.因此,使得混成系統(tǒng)能很好的應(yīng)用于嵌入式系統(tǒng)及其逐步發(fā)展衍生的信息物理融合系統(tǒng)(即CPS)的形式化分析與建模研究之中.隨著信息技術(shù)和制造工程的快速發(fā)展,嵌入式系統(tǒng)和CPS在眾多關(guān)系國(guó)計(jì)民生的安全攸關(guān)領(lǐng)域,如航空航天、智能交通、醫(yī)療衛(wèi)生等均有廣泛應(yīng)用.因而,結(jié)合數(shù)學(xué)與計(jì)算機(jī)方法研究混成系統(tǒng)安全問(wèn)題已成為軟件工程領(lǐng)域的熱門而前沿的研究課題,具有重要的科學(xué)價(jià)值和實(shí)際意義.障礙函數(shù)生成方法作為混成系統(tǒng)安全驗(yàn)證主流方法之一,由于避免了對(duì)混成系統(tǒng)狀態(tài)可達(dá)集計(jì)算的困難而廣受關(guān)注.這類方法關(guān)鍵問(wèn)題在于兩方面,一方面,目前已有的障礙驗(yàn)證條件過(guò)于保守;另一方面,障礙驗(yàn)證條件求解模型計(jì)算復(fù)雜度高.對(duì)此,本文針對(duì)混成系統(tǒng)的障礙函數(shù)生成方法進(jìn)行深入研究,分別從以下三個(gè)角度:創(chuàng)造新的低約束障礙驗(yàn)證條件、簡(jiǎn)化障礙函數(shù)生成模型計(jì)算、復(fù)雜系統(tǒng)模型抽象方法進(jìn)一步降低障礙函數(shù)生成的計(jì)算復(fù)雜度進(jìn)行研究.本論文的主要成果及貢獻(xiàn)有以下幾點(diǎn):·提出新的障礙驗(yàn)證條件構(gòu)造.本文是基于采用Darboux多項(xiàng)式特殊性質(zhì)進(jìn)行構(gòu)造的一類障礙函數(shù),稱為Darboux型障礙函數(shù)生成.由于采用新的安全驗(yàn)證條件構(gòu)造方式,因而能生成已有障礙驗(yàn)證方法所不能生成的障礙函數(shù),通過(guò)實(shí)驗(yàn)結(jié)果也可說(shuō)明這點(diǎn).另外,得益于Darboux型障礙驗(yàn)證條件轉(zhuǎn)化而來(lái)的問(wèn)題模型的特殊特點(diǎn),本文提出一個(gè)LS-QP交叉投影的求解方式,能非常高效的計(jì)算Darboux型障礙函數(shù),實(shí)驗(yàn)結(jié)果能證明本文提出的算法具有高效性.·提出一種新的基于BMI模型求解的障礙函數(shù)生成方法.首先利用SOS松弛方法將經(jīng)典的微分障礙函數(shù)驗(yàn)證模型轉(zhuǎn)化為一類BMI約束求解模型.本文進(jìn)一步針對(duì)一般化BMI約束求解問(wèn)題進(jìn)行研究,最終給出求解一般BMI約束問(wèn)題的變向增廣拉格朗日迭代方法(Alternating Direction Augmented Lagrangian Method)的顯式表達(dá)式.將該結(jié)果用于障礙函數(shù)生成問(wèn)題,并給出求解算法.與當(dāng)前主流軟件PENNON核心算法進(jìn)行比較,本文求解算法復(fù)雜度更低.·提出新的系統(tǒng)抽象方法.針對(duì)復(fù)雜的非線性混成系統(tǒng)模型本身進(jìn)行研究,提出線性抽象的構(gòu)造方法,避免了通過(guò)直接求解復(fù)雜的原系統(tǒng)障礙驗(yàn)證所造成的高計(jì)算復(fù)雜度.將給定的非線性混成系統(tǒng)轉(zhuǎn)化成相應(yīng)的具有待定參數(shù)的線性抽象系統(tǒng),接著對(duì)抽象得到的線性系統(tǒng)運(yùn)用量詞消去方法進(jìn)行線性障礙驗(yàn)證生成,該線性混成系統(tǒng)的安全性同時(shí)保證了原系統(tǒng)的安全性.實(shí)驗(yàn)證明,本文提出的基于線性抽象的障礙函數(shù)生成,能解決原本直接利用量詞消去不能解決的非線性系統(tǒng)安全問(wèn)題.
[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é)位級(jí)別】：博士
【學(xué)位授予年份】：2017
【分類號(hào)】：O19

【相似文獻(xiàn)】

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

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

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

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

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

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

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

7 ;[J];;年期

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

，

本文編號(hào)：1519328