發(fā)布時(shí)間：2018-09-18 14:09

【摘要】：信息-物理融合系統(tǒng)是一種新型嵌入式系統(tǒng)計(jì)算模式.它集成了控制計(jì)算過程和受控對象,二者相互影響并有機(jī)結(jié)合.隨著信息技術(shù)在現(xiàn)實(shí)世界中更加廣泛、深入的應(yīng)用,智能化程度不斷提升,在具有信息-物理緊密耦合特點(diǎn)的嵌入式系統(tǒng)中,嵌入式控制軟件的功能比重急劇上升,作用更加突出.作為安全攸關(guān)的系統(tǒng),需要引入形式化驗(yàn)證方法來保證嵌入式控制應(yīng)用軟件的安全性.基于自動(dòng)機(jī)理論建立統(tǒng)一的系統(tǒng)驗(yàn)證模型,并針對系統(tǒng)的可達(dá)性、安全性(safety)和活性(liveness)等屬性要求,提出了對該模型進(jìn)行形式化驗(yàn)證的算法:基于有界模型檢驗(yàn)方法,基于可達(dá)性將對系統(tǒng)模型的相關(guān)屬性驗(yàn)證問題轉(zhuǎn)換為可滿足性判定問題.將活性轉(zhuǎn)換為Büchi自動(dòng)機(jī),并基于四值語義進(jìn)行判斷.在求解過程中,通過偏序規(guī)約等手段化簡了問題求解的規(guī)模,提高了可驗(yàn)證系統(tǒng)的規(guī)模.另外,結(jié)合協(xié)同仿真技術(shù),靈活配置驗(yàn)證的場景,提高驗(yàn)證的可用性.實(shí)驗(yàn)結(jié)果表明,結(jié)合仿真,形式化協(xié)同驗(yàn)證方法可以有效地對系統(tǒng)進(jìn)行驗(yàn)證.
[Abstract]:Information-physical fusion system is a new embedded system computing mode. It integrates the control computing process and the controlled object, and they interact with each other and combine organically. With the more extensive and in-depth application of information technology in the real world, the degree of intelligence has been improved continuously, and the function proportion of embedded control software has risen sharply in the embedded system with the characteristics of information and physical tight coupling. The role is more prominent. As a security related system, formal verification method should be introduced to ensure the security of embedded control applications. Based on the automata theory, a unified system verification model is established. According to the requirements of reachability, security (safety) and active (liveness), an algorithm for formal verification of the model is proposed: based on the bounded model checking method. Based on reachability, the problem of attribute verification for system model is transformed into satisfiability decision problem. The activity is converted to B 眉 chi automaton and judged on the basis of quaternary semantics. In the process of solving the problem, the scale of problem solving is simplified by means of partial order protocol, and the scale of verifiable system is improved. In addition, combined with collaborative simulation technology, the scenario of verification can be configured flexibly to improve the availability of verification. The experimental results show that the formal collaborative verification method can effectively validate the system.
【作者單位】： 南海海洋資源利用國家重點(diǎn)實(shí)驗(yàn)室(海南大學(xué));海南大學(xué)信息科學(xué)技術(shù)學(xué)院;西北工業(yè)大學(xué)計(jì)算機(jī)學(xué)院;
【基金】：國家自然科學(xué)基金(61462022,61363071) 國家科技支撐計(jì)劃(2014BAD10B04,2015BAH55F04) 海南省重大科技計(jì)劃(ZDKJ2016015) 海南省自然科學(xué)基金(614232,614220) 海南省產(chǎn)學(xué)研一體化專項(xiàng)(cxy20150025) 海南大學(xué)科研啟動(dòng)基金(kyqd1610)~~
【分類號】：TP311.1

【參考文獻(xiàn)】

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

1 單黎君;周興社;王宇英;趙雷;萬麗景;喬磊;陳建新;;信息物理融合系統(tǒng)控制軟件的統(tǒng)計(jì)模型檢驗(yàn)[J];軟件學(xué)報(bào);2015年02期

【共引文獻(xiàn)】

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

1 張雨;董云衛(wèi);馮文龍;黃夢醒;;一種面向CPS的控制應(yīng)用程序協(xié)同驗(yàn)證方法[J];軟件學(xué)報(bào);2017年05期

2 周顯芳;;省級國土資源綜合統(tǒng)計(jì)分析系統(tǒng)研究[J];軟件工程;2016年07期

【相似文獻(xiàn)】

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

1 宋文,嚴(yán)兵,潘世永;對自動(dòng)機(jī)與形式語言中幾個(gè)問題的思考[J];四川工業(yè)學(xué)院學(xué)報(bào);2002年04期

2 劉光武;石曉龍;許進(jìn);;賦權(quán)型自動(dòng)機(jī)的不同模型研究[J];計(jì)算機(jī)工程與應(yīng)用;2006年11期

3 蔡國永;錢俊彥;;關(guān)于形式語言與自動(dòng)機(jī)理論的教學(xué)方法探討[J];高教論壇;2008年04期

4 郭瑞楓;;半自動(dòng)機(jī)理論在(漢字)辭庫建造中的應(yīng)用[J];南京大學(xué)學(xué)報(bào)(自然科學(xué)版);1984年03期

5 邱道文;量子自動(dòng)機(jī)的刻畫[J];軟件學(xué)報(bào);2003年01期

6 周清雷;朱維軍;趙東明;;時(shí)間ω-樹自動(dòng)機(jī)識別語言的一個(gè)條件[J];信陽師范學(xué)院學(xué)報(bào)(自然科學(xué)版);2006年04期

7 謝清;譚建榮;馮毅雄;;基于自動(dòng)機(jī)的可配置產(chǎn)品功構(gòu)映射過程研究[J];計(jì)算機(jī)集成制造系統(tǒng);2007年09期

8 趙嶺忠;王雪松;錢俊彥;;改進(jìn)形式語言與自動(dòng)機(jī)理論課程教學(xué)芻議[J];高教論壇;2008年03期

9 錢俊彥;趙嶺忠;;基于自動(dòng)機(jī)理論的符號模型檢驗(yàn)[J];蘭州理工大學(xué)學(xué)報(bào);2008年05期

10 劉建國;袁志斌;;基于左右語言的狀態(tài)遷移系統(tǒng)的優(yōu)化[J];計(jì)算機(jī)科學(xué);2009年05期

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

1 西廣成;;抽象神經(jīng)自動(dòng)機(jī)演化過程中熵極限性質(zhì)[A];1999年中國神經(jīng)網(wǎng)絡(luò)與信號處理學(xué)術(shù)會(huì)議論文集[C];1999年

2 蘇仕云;郭瑞強(qiáng);樂嘉錦;;有窮狀態(tài)自動(dòng)機(jī)在商業(yè)邏輯建模中的應(yīng)用[A];第十九屆全國數(shù)據(jù)庫學(xué)術(shù)會(huì)議論文集（研究報(bào)告篇）[C];2002年

3 陽斌;秦琳琳;吳剛;;基于混雜自動(dòng)機(jī)的溫室溫度系統(tǒng)建模與控制[A];中國自動(dòng)化學(xué)會(huì)控制理論專業(yè)委員會(huì)D卷[C];2011年

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

1 徐慧;自動(dòng)機(jī)的代數(shù)表示和形式語言的研究[D];西北大學(xué);2015年

2 田徑;關(guān)于自動(dòng)機(jī)代數(shù)理論的研究[D];西北大學(xué);2012年

3 劉光武;自動(dòng)機(jī)狀態(tài)復(fù)雜度及模型研究[D];華中科技大學(xué);2007年

4 文艷軍;基于接口自動(dòng)機(jī)的組合驗(yàn)證方法研究[D];國防科學(xué)技術(shù)大學(xué);2005年

5 張薇;自動(dòng)機(jī)和鏈編碼的理論研究與應(yīng)用[D];華東師范大學(xué);2006年

6 李丹美;模糊離散事件自動(dòng)機(jī)組合的控制與切換[D];東華大學(xué);2009年

7 陳文宇;形式語言與自動(dòng)機(jī)理論若干問題研究[D];電子科技大學(xué);2009年

8 韓召偉;幾類基于量子邏輯的自動(dòng)機(jī)的代數(shù)及邏輯刻畫[D];陜西師范大學(xué);2011年

9 沈潔;基于自動(dòng)機(jī)的XML數(shù)據(jù)過濾研究[D];哈爾濱工程大學(xué);2010年

10 巨志勇;基于動(dòng)態(tài)系統(tǒng)計(jì)算的數(shù)字圖像處理[D];同濟(jì)大學(xué);2007年

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

1 陳晴雷;量子自動(dòng)機(jī)的乘積研究[D];四川師范大學(xué);2012年

2 朱鏡儒;光伏電源三相混聯(lián)接入系統(tǒng)混成自動(dòng)機(jī)控制研究[D];長沙理工大學(xué);2014年

3 周戈;基于運(yùn)行時(shí)驗(yàn)證的監(jiān)控器生成技術(shù)研究[D];國防科學(xué)技術(shù)大學(xué);2014年

4 宋俊;LTLNFBA:LTL公式到Büchi自動(dòng)機(jī)的轉(zhuǎn)換[D];西安電子科技大學(xué);2014年

5 趙庚兵;基于自動(dòng)機(jī)理論的軟件項(xiàng)目進(jìn)度監(jiān)控方法研究[D];廣東工業(yè)大學(xué);2016年

6 李慧水;某新型重載高速自動(dòng)機(jī)動(dòng)力學(xué)分析[D];南京理工大學(xué);2016年

7 凌駿;大規(guī)模RDF圖數(shù)據(jù)的屬性路徑查詢及推理研究[D];天津大學(xué);2014年

8 王向飛;基于自動(dòng)機(jī)理論的鋼鐵線材打包機(jī)控制軟件設(shè)計(jì)[D];浙江工業(yè)大學(xué);2016年

9 張博;廣義可能線性時(shí)序邏輯的自動(dòng)機(jī)方法[D];陜西師范大學(xué);2016年

10 石文兵;基于自動(dòng)機(jī)的交易系統(tǒng)設(shè)計(jì)研究[D];西北師范大學(xué);2016年

，

本文編號：2248158