本文關(guān)鍵詞：以DNA為載體的線性時序邏輯模型檢測

  更多相關(guān)文章： 模型檢測 脫氧核糖核酸 線性時序邏輯 粘貼自動機

【摘要】：線性時序邏輯模型檢測被廣泛應(yīng)用于處理器設(shè)計與驗證、網(wǎng)絡(luò)協(xié)議驗證、安全協(xié)議驗證等領(lǐng)域.然而到目前為止,該技術(shù)只能在電子計算的平臺上實現(xiàn).為了以脫氧核糖核酸(Deoxyribo Nucleic Acid,DNA)為載體對線性時序邏輯(Linear Temporal Logic,LTL)實施模型檢測,給出了使用粘貼自動機實現(xiàn)Until算子模型檢測的方法.首先,使用粘貼自動機對Until公式的有窮狀態(tài)自動機(Finite State Automata,FSA)模型進行編碼;然后,將系統(tǒng)模型轉(zhuǎn)換為粘貼自動機的輸入字符串;最后,用粘貼自動機驗證系統(tǒng)是否滿足公式.仿真實驗結(jié)果證實,新方法可實現(xiàn)對LTL邏輯時序算子的檢測.
【作者單位】： 鄭州大學信息工程學院;
【關(guān)鍵詞】： 模型檢測 脫氧核糖核酸 線性時序邏輯 粘貼自動機
【基金】：國家自然科學基金(No.61250007,No.U1204608,No.U1304606,No.61572444) 中國博士后科學基金(No.2012M511588,No.2015M572120) 河南省高等學校青年骨干教師資助計劃項目(No.2014GGJS-001)
【分類號】：TP301.1
【正文快照】： 1引言模型檢測由圖靈獎得主Clarke教授等人提出[1].它是一種能夠自動驗證系統(tǒng)是否滿足給定性質(zhì)的形式化核心方法與技術(shù),被廣泛地應(yīng)用于硬件驗證[2]、網(wǎng)絡(luò)協(xié)議驗證、安全協(xié)議驗證[3]等領(lǐng)域.在時序邏輯模型檢測中,線性時序邏輯[4](Linear Temporal Logic,LTL)、計算樹邏輯[5](Co

【相似文獻】

中國期刊全文數(shù)據(jù)庫 前10條

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

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

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

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

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

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

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

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

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

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

中國重要會議論文全文數(shù)據(jù)庫 前5條

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

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

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

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

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

中國博士學位論文全文數(shù)據(jù)庫 前10條

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

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

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

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

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

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

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

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

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

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

中國碩士學位論文全文數(shù)據(jù)庫 前10條

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

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

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

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

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

6 鄧楠軼;基于廣義可能性測度的模型檢測器GPoCheck的設(shè)計與實現(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年

，

本文編號：553425