本文關(guān)鍵詞：信息物理融合系統(tǒng)安全性驗(yàn)證研究　出處：《華東師范大學(xué)》2016年博士論文　論文類(lèi)型：學(xué)位論文

  更多相關(guān)文章： 信息物理融合系統(tǒng) 混成系統(tǒng) 安全性驗(yàn)證 形式化方法 柵欄函數(shù)

【摘要】：安全性問(wèn)題貫穿信息物理融合系統(tǒng)建模、分析、設(shè)計(jì)、開(kāi)發(fā)與維護(hù)整個(gè)系統(tǒng)生命周期。信息物理融合系統(tǒng)中的安全性問(wèn)題內(nèi)涵豐富、形式多樣、廣泛存在。本文基于動(dòng)力系統(tǒng)的視角,以混成系統(tǒng)建模信息物理融合系統(tǒng)動(dòng)力學(xué)過(guò)程,形式化的界定信息物理融合系統(tǒng)安全性問(wèn)題為相應(yīng)混成系統(tǒng)狀態(tài)軌線(xiàn)與系統(tǒng)規(guī)約不安全點(diǎn)集相交性判定。信息物理融合系統(tǒng)生命周期涵蓋多個(gè)階段,每個(gè)階段存在不同場(chǎng)景。這種狀況造成信息物理融合系統(tǒng)安全性問(wèn)題雖內(nèi)涵統(tǒng)一,但具體存在形式卻千差萬(wàn)別。把握決定系統(tǒng)安全性的主要因素,合理抽象安全性驗(yàn)證情景是信息物理融合系統(tǒng)安全性驗(yàn)證研究的前提和基礎(chǔ)。總體來(lái)說(shuō),系統(tǒng)行為機(jī)制、控制機(jī)制和結(jié)構(gòu)機(jī)制是影響系統(tǒng)安全性狀況的關(guān)鍵因素。有鑒于此,信息物理融合系統(tǒng)安全性驗(yàn)證可以抽象為針對(duì)混成系統(tǒng)特定行為機(jī)制、控制機(jī)制與結(jié)構(gòu)機(jī)制安全性的判定�；谶@樣的認(rèn)識(shí),本文以信息物理融合系統(tǒng)為背景,面向系統(tǒng)安全性驗(yàn)證問(wèn)題,致力于發(fā)展以混成系統(tǒng)行為機(jī)制、控制機(jī)制與結(jié)構(gòu)機(jī)制等的安全性為核心的形式化驗(yàn)證理論與方法。系統(tǒng)狀態(tài)的連續(xù)演化、脈沖跳變與模式切換是混成系統(tǒng)行為的基本形式,三者在狀態(tài)空間劃分約束下的交互構(gòu)成了混成系統(tǒng)行為機(jī)制的內(nèi)容。針對(duì)混成系統(tǒng)行為機(jī)制安全性,本文介紹了以柵欄函數(shù)(barrier certificates)定理為核心的安全性判定理論和以柵欄函數(shù)構(gòu)造定理為核心的判定方法。閉環(huán)的反饋控制與開(kāi)環(huán)的駐留時(shí)間控制是混成系統(tǒng)控制的基本形式,狀態(tài)反饋控制與駐留時(shí)間約束是混成系統(tǒng)控制機(jī)制的主要內(nèi)容。本文選取模式相關(guān)駐留時(shí)間切換策略與區(qū)間駐留時(shí)間切換策略為控制機(jī)制安全性驗(yàn)證研究的對(duì)象,分別給出相應(yīng)的柵欄函數(shù)定理及其構(gòu)造定理,發(fā)展針對(duì)這兩種駐留時(shí)間驅(qū)動(dòng)控制機(jī)制安全性驗(yàn)證的理論與方法。切換型混成系統(tǒng)的串級(jí)與脈沖型混成系統(tǒng)的串級(jí)是串級(jí)混成系統(tǒng)結(jié)構(gòu)的兩種基本形式。本文針對(duì)串級(jí)切換型混成系統(tǒng)與串級(jí)脈沖型混成系統(tǒng)安全性的判定問(wèn)題,分別給出相應(yīng)柵欄函數(shù)定理及其構(gòu)造定理,為系統(tǒng)結(jié)構(gòu)機(jī)制安全性驗(yàn)證提供了從判定原理到判定方法的完整解決方案。全文研究工作以模式相關(guān)駐留時(shí)間切換策略、區(qū)間駐留時(shí)間切換策略、串級(jí)切換型混成系統(tǒng)與串級(jí)脈沖型混成系統(tǒng)安全性驗(yàn)證的解決為核心,從下四個(gè)方面完善信息物理融合系統(tǒng)安全性驗(yàn)證的研究：首先,針對(duì)混成系統(tǒng)行為機(jī)制安全性驗(yàn)證問(wèn)題,本文以混成動(dòng)力系統(tǒng)模型為基礎(chǔ),形式化的定義了混成系統(tǒng)行為,通過(guò)柵欄函數(shù)定理,論證柵欄函數(shù)存在則混成系統(tǒng)安全這一命題。進(jìn)一步地,就柵欄函數(shù)的構(gòu)造,介紹了柵欄函數(shù)構(gòu)造定理及相關(guān)理論、方法和工具。其次,針對(duì)混成系統(tǒng)控制機(jī)制安全性驗(yàn)證問(wèn)題,本文以駐留時(shí)間控制機(jī)制為研究對(duì)象,形式化的討論模式相關(guān)駐留時(shí)間切換策略與區(qū)間駐留時(shí)間切換策略安全性的判定條件,給出相應(yīng)柵欄函數(shù)定理。結(jié)合駐留時(shí)間約束控制機(jī)制柵欄函數(shù)的特點(diǎn),給定相應(yīng)柵欄函數(shù)構(gòu)造定理,降低柵欄函數(shù)構(gòu)造中的計(jì)算困難性。再次,針對(duì)混成系統(tǒng)結(jié)構(gòu)機(jī)制安全性驗(yàn)證問(wèn)題,本文以串級(jí)結(jié)構(gòu)機(jī)制為研究對(duì)象,形式化的討論串級(jí)切換型混成系統(tǒng)與串級(jí)脈沖型混成系統(tǒng)安全性判定條件,結(jié)合各自系統(tǒng)結(jié)構(gòu)特點(diǎn),通過(guò)引入類(lèi)耗散不等式與小增益條件等約束,構(gòu)造確保系統(tǒng)安全的充分條件,給出相應(yīng)柵欄函數(shù)定理。進(jìn)一步地,給出相應(yīng)柵欄函數(shù)構(gòu)造定理,促進(jìn)系統(tǒng)結(jié)構(gòu)機(jī)制安全性驗(yàn)證問(wèn)題的自動(dòng)化解決。最后,針對(duì)一種基于向量Lyapunov函數(shù)方法設(shè)計(jì)的顧前顧后型車(chē)輛跟隨反饋控制律的“防碰撞”安全需求的驗(yàn)證問(wèn)題,給出基于柵欄函數(shù)的驗(yàn)證方法。
[Abstract]:Safety problems through the physical information fusion system modeling, analysis, design, development and maintenance of the whole system life cycle. The connotation of physical information fusion system security in the rich, diverse forms, widely exist. This paper based on the perspective of power system, the hybrid system modeling physical information fusion system dynamic process, the formal definition of information physical system security problem to determine the corresponding intersection of the trajectory of hybrid system and system security statute does not set. Physical information fusion system life cycle covers multiple stages, each stage in different scenes. This situation caused by the physical information fusion system security problem is the connotation of unity, but the forms are different. To grasp the decision the main factors of system safety, reasonable abstract security verification scenario is the study of system security verification before physical information fusion And provided basis. In general, the behavior of the system mechanism, control mechanism and structure mechanism is a key factor affecting the system security situation. In view of this, the physical information fusion system security verification can be abstracted as the specific behavior of hybrid system, decision control mechanism and structure of system security. Based on this understanding, this paper based on information physical system as the background, system oriented security verification, committed to the development of the hybrid system behavior mechanism, security mechanism and control mechanism of the structure is the core of the formal verification theory and method. The continuous evolution of the system state, pulse and mode switching is the basic form of hybrid system behavior, interaction three in the state space partition constraints constitute a hybrid system behavior mechanism of the content. For the hybrid system security mechanism, this paper introduces the barrier function (bar Rier certificates) safety decision theorem as the core of the theories and methods on barrier function structure theorem as the core. The closed-loop feedback control and open-loop control of dwell time is the basic form of hybrid system control, state feedback control and dwell time constraints is the main content of hybrid system control mechanism. This paper selects patterns related to reside time switching strategy and interval dwell time switching strategy to control the mechanism to verify the safety of the object of study, were given the barrier function theorem and its structure theorem, the development of the two kinds of dwell time drive theory and method of control mechanism for security verification. Cascade switched hybrid system with cascade pulse type hybrid system is on the two basic forms of hybrid system level structure. In this paper the cascade switched hybrid system with cascade safety type hybrid system pulse judgment Fixed problem are given the corresponding barrier function theorem and its structure theorem, provides a solution to the principle from the judging method to determine the complete solution for system security verification. The mechanism and structure of the research work related to mode of dwell time switching strategy, interval dwell time switching strategy, cascade switched hybrid systems and solve the security level pulse string hybrid system verification is the core of information fusion system, physical security verification perfect from the following four aspects: first, the hybrid system behavior and mechanism of the safety verification problem, based on the hybrid power system model, the formalization of hybrid system behavior, through the fence function theorem, proof fence function is this hybrid system security proposition. Further, the structural barrier function, the barrier function construction theorem and the related theories, methods and tools. Time for hybrid system verification of safety control mechanism, based on the dwell time control mechanism as the research object, formal discussion mode related dwell time switching strategy and interval dwell time switching strategy safety conditions, the corresponding barrier function theorem. Combining the dwell time constraint control mechanism of barrier function, given the corresponding structure the fence function theorem, reduce the difficulty of computing the barrier function structure. Thirdly, according to the structure of hybrid system security mechanism based on the verification problem, cascade structure mechanism as the research object, discuss the form of cascade switched hybrid system with cascade pulse type hybrid system safety conditions, combined with their structural characteristics of the system, by introducing dissipative inequality and small gain conditions and other constraints, sufficient conditions to ensure the security of the system structure, the corresponding fence function theorem. Further, the corresponding structural barrier function theorem, promote automation system structure security verification mechanism to solve the problem. Finally, according to the design of a vector Lyapunov function method of front and back information vehicle following feedback control law based on the "collision" safety requirements verification problem, given verification method based on the function of the fence.

【學(xué)位授予單位】：華東師范大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2016
【分類(lèi)號(hào)】：TP309

【相似文獻(xiàn)】

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

1 李浪;李仁發(fā);李肯立;姚鳳娟;;混成系統(tǒng)研究綜述[J];計(jì)算機(jī)應(yīng)用研究;2008年08期

2 侯建民,鄭滔,樊曉聰,李宣東,鄭國(guó)梁;線(xiàn)性混成系統(tǒng)的參數(shù)分析[J];計(jì)算機(jī)學(xué)報(bào);1999年06期

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

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

5 卜磊;解定寶;;混成系統(tǒng)形式化驗(yàn)證[J];軟件學(xué)報(bào);2014年02期

6 喬磊;齊驥;龔育昌;;一種支持可重構(gòu)混成系統(tǒng)的操作系統(tǒng)設(shè)計(jì)與實(shí)現(xiàn)[J];計(jì)算機(jī)學(xué)報(bào);2009年05期

7 趙劍;歐陽(yáng)丹彤;王曉宇;張立明;;混成系統(tǒng)的分布式診斷方法[J];吉林大學(xué)學(xué)報(bào)(工學(xué)版);2012年06期

8 肖娟;;混成系統(tǒng)的形式驗(yàn)證[J];長(zhǎng)沙通信職業(yè)技術(shù)學(xué)院學(xué)報(bào);2008年01期

9 葉林;湯瀑;郭立鵬;張亮;;基于混成系統(tǒng)的物聯(lián)網(wǎng)服務(wù)建模與驗(yàn)證[J];小型微型計(jì)算機(jī)系統(tǒng);2013年12期

10 閻安,唐稚松;基于 XYZ/ E的混成系統(tǒng)(英文)[J];軟件學(xué)報(bào);2000年01期

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

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

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

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

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

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

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

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

6 李廣元;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ǔ)義的線(xiàn)性混成系統(tǒng)分析[D];南京大學(xué);2013年

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

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

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

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

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

，

本文編號(hào)：1412106