本文選題：形式化方法 + 形式化驗(yàn)證�。� 參考：《軍事通信技術(shù)》2016年02期

【摘要】：隨著計(jì)算機(jī)系統(tǒng)的功能日益強(qiáng)大,對(duì)其進(jìn)行功能和正確性測(cè)試與驗(yàn)證的復(fù)雜度也越來(lái)越大。形式化方法作為對(duì)計(jì)算機(jī)系統(tǒng)進(jìn)行描述與驗(yàn)證的重要途徑,得到學(xué)術(shù)界普遍的關(guān)注與認(rèn)可。文章主要介紹形式化方法,詳細(xì)介紹模型檢測(cè)的檢測(cè)原理及其主要技術(shù),介紹了幾種典型的模型檢測(cè)工具,并對(duì)它們的性能進(jìn)行比較,同時(shí)研究了模型檢測(cè)中普遍存在的狀態(tài)爆炸問(wèn)題及縮減狀態(tài)方法,最后介紹模型檢測(cè)的新進(jìn)展。文章可為模型檢測(cè)方法研究提供參考和理論支撐。
[Abstract]:With the increasingly powerful functions of computer systems, the complexity of testing and verifying their functions and correctness is increasing. As an important way to describe and verify computer systems, formal methods have received widespread attention and recognition in academic circles. This paper mainly introduces the formal method, introduces the detection principle and main technology of model checking in detail, introduces several typical model checking tools, and compares their performance. At the same time, the problem of state explosion and the method of state reduction are studied. Finally, the new progress of model detection is introduced. This paper can provide reference and theoretical support for the research of model detection method.
【作者單位】： 解放軍理工大學(xué)指揮信息系統(tǒng)學(xué)院研究生1隊(duì);解放軍理工大學(xué)指揮信息系統(tǒng)學(xué)院;
【分類號(hào)】：TP302.7

【相似文獻(xiàn)】

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

1 戎玫;張廣泉;;模型檢測(cè)新技術(shù)研究[J];計(jì)算機(jī)科學(xué);2003年05期

2 肖健宇;張德運(yùn);鄭衛(wèi)斌;;過(guò)程提取用于改善程序模型檢測(cè)的可伸縮性[J];西安交通大學(xué)學(xué)報(bào);2006年06期

3 袁志斌;徐正權(quán);王能超;;軟件模型檢測(cè)中的抽象[J];計(jì)算機(jī)科學(xué);2006年07期

4 劉吉鋒;孫吉貴;;基于抽象-驗(yàn)證-細(xì)化范例的軟件模型檢測(cè)[J];計(jì)算機(jī)科學(xué);2006年12期

5 化志章;吳傳孫;揭安全;薛錦云;;軟件模型檢測(cè)新技術(shù)研究[J];微計(jì)算機(jī)信息;2007年36期

6 王飛明;胡元闖;董榮勝;;模型檢測(cè)研究進(jìn)展[J];廣西科學(xué)院學(xué)報(bào);2008年04期

7 鄺宏斌;羅貴明;;并行軟件模型檢測(cè)[J];計(jì)算機(jī)工程;2008年19期

8 何愷鐸;顧明;宋曉宇;李力;李江;;面向源代碼的軟件模型檢測(cè)及其實(shí)現(xiàn)[J];計(jì)算機(jī)科學(xué);2009年01期

9 林璇;;模型檢測(cè)方法在入侵檢測(cè)中的應(yīng)用研究[J];現(xiàn)代計(jì)算機(jī)(專業(yè)版);2009年02期

10 顧濱兵;;一種軟件模型檢測(cè)方法及其原型系統(tǒng)[J];微計(jì)算機(jī)應(yīng)用;2010年11期

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

1 高靜;曹子寧;;基于空間邏輯和計(jì)算樹(shù)邏輯的模型檢測(cè)[A];2009年中國(guó)高校通信類院系學(xué)術(shù)研討會(huì)論文集[C];2009年

2 許梅;曹子寧;;基于謂詞μ演算和空間邏輯的模型檢測(cè)算法研究[A];2009年中國(guó)高校通信類院系學(xué)術(shù)研討會(huì)論文集[C];2009年

3 何青;駱翔宇;蘇開(kāi)樂(lè);;對(duì)弈必勝策略的符號(hào)化模型檢測(cè)[A];2006年全國(guó)理論計(jì)算機(jī)科學(xué)學(xué)術(shù)年會(huì)論文集[C];2006年

4 王飛明;胡元闖;董榮勝;;模型檢測(cè)中狀態(tài)爆炸及其優(yōu)化策略研究[A];廣西計(jì)算機(jī)學(xué)會(huì)2008年年會(huì)論文集[C];2008年

5 陳道喜;張廣泉;陳冬火;;NSPK協(xié)議的Spin模型檢測(cè)[A];2008年全國(guó)開(kāi)放式分布與并行計(jì)算機(jī)學(xué)術(shù)會(huì)議論文集(下冊(cè))[C];2008年

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

1 奚琪;基于模型檢測(cè)的二進(jìn)制代碼惡意行為識(shí)別技術(shù)研究[D];解放軍信息工程大學(xué);2014年

2 江華;界程演算模型檢測(cè)[D];貴州大學(xué);2008年

3 林榮德;移動(dòng)界程演算及模型檢測(cè)應(yīng)用的關(guān)鍵問(wèn)題研究[D];華南理工大學(xué);2010年

4 劉劍;傳值進(jìn)程與移動(dòng)進(jìn)程的模型檢測(cè)方法[D];中國(guó)科學(xué)院研究生院（軟件研究所）;2005年

5 劉志鋒;模型檢測(cè)中關(guān)鍵技術(shù)的研究及其應(yīng)用[D];南京大學(xué);2011年

6 朱維軍;時(shí)間區(qū)間時(shí)序邏輯模型檢測(cè)：理論、算法及應(yīng)用[D];西安電子科技大學(xué);2011年

7 尹良澤;基于SAT的組合遷移系統(tǒng)模型檢測(cè)技術(shù)研究[D];清華大學(xué);2014年

8 陳冬火;超協(xié)調(diào)時(shí)序邏輯及其模型檢測(cè)方法[D];中國(guó)科學(xué)院研究生院（成都計(jì)算機(jī)應(yīng)用研究所）;2006年

9 田聰;命題投影時(shí)序邏輯的判定性、復(fù)雜性、表達(dá)性及模型檢測(cè)[D];西安電子科技大學(xué);2010年

10 黃宏濤;基于懶惰切片的模型檢測(cè)技術(shù)研究[D];哈爾濱工程大學(xué);2012年

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

1 李永亮;基于DNA計(jì)算的CTL模型檢測(cè)方法研究[D];鄭州大學(xué);2015年

2 楊樹(shù)峰;基于統(tǒng)計(jì)模型檢測(cè)的無(wú)線傳感器網(wǎng)絡(luò)協(xié)議建模與分析[D];鄭州大學(xué);2015年

3 張興興;基于廣義可能性測(cè)度的互模擬及CTL不動(dòng)點(diǎn)語(yǔ)義[D];陜西師范大學(xué);2015年

4 王彬;基于多值模型檢測(cè)的SaaS應(yīng)用測(cè)試及其自動(dòng)化研究[D];陜西師范大學(xué);2015年

5 王凱;基于模型檢測(cè)多反例對(duì)軟件進(jìn)行調(diào)試[D];電子科技大學(xué);2015年

6 鄧楠軼;基于廣義可能性測(cè)度的模型檢測(cè)器GPoCheck的設(shè)計(jì)與實(shí)現(xiàn)[D];陜西師范大學(xué);2015年

7 張恒;多值模型檢測(cè)器的研究與實(shí)現(xiàn)[D];陜西師范大學(xué);2015年

8 高毅;不同模型檢測(cè)下信號(hào)并串轉(zhuǎn)換模塊功能建模的研究[D];電子科技大學(xué);2014年

9 崔曉爽;基于GSTE模型檢測(cè)的信號(hào)并串轉(zhuǎn)換模塊功能驗(yàn)證的研究[D];電子科技大學(xué);2014年

10 許落汀;基于BDDs的離散實(shí)時(shí)時(shí)態(tài)邏輯RTCTL*的符號(hào)化模型檢測(cè)及證據(jù)生成[D];華僑大學(xué);2015年

，

本文編號(hào)：1948245