本文選題：形式化方法 + 形式化驗證　； 參考：《軍事通信技術》2016年02期

【摘要】：隨著計算機系統(tǒng)的功能日益強大,對其進行功能和正確性測試與驗證的復雜度也越來越大。形式化方法作為對計算機系統(tǒng)進行描述與驗證的重要途徑,得到學術界普遍的關注與認可。文章主要介紹形式化方法,詳細介紹模型檢測的檢測原理及其主要技術,介紹了幾種典型的模型檢測工具,并對它們的性能進行比較,同時研究了模型檢測中普遍存在的狀態(tài)爆炸問題及縮減狀態(tài)方法,最后介紹模型檢測的新進展。文章可為模型檢測方法研究提供參考和理論支撐。
[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.
【作者單位】： 解放軍理工大學指揮信息系統(tǒng)學院研究生1隊;解放軍理工大學指揮信息系統(tǒng)學院;
【分類號】：TP302.7

【相似文獻】

相關期刊論文 前10條

1 戎玫;張廣泉;;模型檢測新技術研究[J];計算機科學;2003年05期

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

3 袁志斌;徐正權;王能超;;軟件模型檢測中的抽象[J];計算機科學;2006年07期

4 劉吉鋒;孫吉貴;;基于抽象-驗證-細化范例的軟件模型檢測[J];計算機科學;2006年12期

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

6 王飛明;胡元闖;董榮勝;;模型檢測研究進展[J];廣西科學院學報;2008年04期

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

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

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

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

相關會議論文 前5條

1 高靜;曹子寧;;基于空間邏輯和計算樹邏輯的模型檢測[A];2009年中國高校通信類院系學術研討會論文集[C];2009年

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

3 何青;駱翔宇;蘇開樂;;對弈必勝策略的符號化模型檢測[A];2006年全國理論計算機科學學術年會論文集[C];2006年

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

5 陳道喜;張廣泉;陳冬火;;NSPK協(xié)議的Spin模型檢測[A];2008年全國開放式分布與并行計算機學術會議論文集(下冊)[C];2008年

相關博士學位論文 前10條

1 奚琪;基于模型檢測的二進制代碼惡意行為識別技術研究[D];解放軍信息工程大學;2014年

2 江華;界程演算模型檢測[D];貴州大學;2008年

3 林榮德;移動界程演算及模型檢測應用的關鍵問題研究[D];華南理工大學;2010年

4 劉劍;傳值進程與移動進程的模型檢測方法[D];中國科學院研究生院（軟件研究所）;2005年

5 劉志鋒;模型檢測中關鍵技術的研究及其應用[D];南京大學;2011年

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

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

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

9 田聰;命題投影時序邏輯的判定性、復雜性、表達性及模型檢測[D];西安電子科技大學;2010年

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

相關碩士學位論文 前10條

1 李永亮;基于DNA計算的CTL模型檢測方法研究[D];鄭州大學;2015年

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

3 張興興;基于廣義可能性測度的互模擬及CTL不動點語義[D];陜西師范大學;2015年

4 王彬;基于多值模型檢測的SaaS應用測試及其自動化研究[D];陜西師范大學;2015年

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

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

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

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

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

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

，

本文編號：1948245