本文關(guān)鍵詞： 統(tǒng)一模型檢測(cè) 實(shí)時(shí)系統(tǒng) 可滿足性判定 時(shí)間區(qū)間時(shí)序邏輯　出處：《電子科技大學(xué)學(xué)報(bào)》2014年05期 　論文類型：期刊論文

【摘要】：在同一個(gè)邏輯框架內(nèi)無法自動(dòng)驗(yàn)證實(shí)時(shí)區(qū)間模型的實(shí)時(shí)區(qū)間性質(zhì)。為此,該文使用一個(gè)離散時(shí)間區(qū)間時(shí)序邏輯公式建立實(shí)時(shí)系統(tǒng)模型,使用另一個(gè)離散時(shí)間區(qū)間時(shí)序邏輯公式描述實(shí)時(shí)系統(tǒng)需要滿足的性質(zhì),在此基礎(chǔ)上,離散時(shí)間區(qū)間時(shí)序邏輯統(tǒng)一模型檢測(cè)問題即可歸約為目前已解決的離散時(shí)間區(qū)間時(shí)序邏輯可滿足性判定問題。該文證明了新方法的有效性以及正確性,為區(qū)間實(shí)時(shí)邏輯這一類的模型檢測(cè)問題提供了方法。
[Abstract]:The real time interval property of the real time interval model can not be automatically verified in the same logic framework. In this paper, a discrete time interval temporal logic formula is used to establish the real time system model. Another discrete time interval temporal logic formula is used to describe the properties of real-time systems. The unified model checking problem of discrete time interval temporal logic can be reduced to the discrete-time interval temporal logic satisfiability judgment problem which has been solved at present. This paper proves the validity and correctness of the new method. It provides a method for model checking problems such as interval real-time logic.
【作者單位】： 鄭州大學(xué)信息工程學(xué)院;西安電子科技大學(xué)計(jì)算機(jī)學(xué)院;河南牧業(yè)經(jīng)濟(jì)學(xué)院信息工程系;
【基金】：國(guó)家自然科學(xué)基金(U1204608,U1304606,61373043) 中國(guó)博士后科學(xué)基金(2012M511588)
【分類號(hào)】：TP301;TP306
【正文快照】： Model Checking Real-Time Systems within Unified Approachof Timed Interval Temporal Logic模型檢測(cè)(model checking,MC)是一種自動(dòng)驗(yàn)證系統(tǒng)性質(zhì)的形式化技術(shù),得到了廣泛關(guān)注、研究與使用。在實(shí)時(shí)計(jì)算模型檢測(cè)領(lǐng)域,時(shí)間自動(dòng)機(jī)(timedautomata,TA)[1]已成為建立模型的事實(shí)標(biāo)

【相似文獻(xiàn)】

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

1 劉瑞挺;;自動(dòng)驗(yàn)證技術(shù)獲得圖靈獎(jiǎng)[J];計(jì)算機(jī)教育;2008年23期

2 朱明,邊計(jì)年,吳為民;基于CDFG和OVL的系統(tǒng)驗(yàn)證性質(zhì)分類[J];計(jì)算機(jī)工程;2005年10期

3 白金山;崔楠;李祥;;行為時(shí)態(tài)邏輯TLA定理系統(tǒng)證明及公平性研究[J];計(jì)算機(jī)工程與設(shè)計(jì);2010年03期

4 張軼,林惠民;帶復(fù)雜數(shù)據(jù)結(jié)構(gòu)的模型檢測(cè)工具[J];計(jì)算機(jī)研究與發(fā)展;2004年11期

5 化志章;揭安全;薛錦云;;一種自動(dòng)的形式化驗(yàn)證技術(shù)——模型檢測(cè)[J];微計(jì)算機(jī)信息;2007年33期

6 呂正;陳昊;陳峰;呂毅;;模型檢測(cè)MESIF Cache一致性協(xié)議[J];計(jì)算機(jī)工程與應(yīng)用;2010年17期

7 吳立軍;駱翔宇;陳清亮;;基于動(dòng)態(tài)內(nèi)存和狀態(tài)管理的模型檢測(cè)新方法[J];計(jì)算機(jī)科學(xué);2011年11期

8 肖美華;熊昊;;模型檢測(cè)中反例最小化分析[J];南昌大學(xué)學(xué)報(bào)(工科版);2008年04期

9 郭陽,李暾,李思昆;微處理器功能驗(yàn)證方法研究[J];計(jì)算機(jī)工程與應(yīng)用;2003年05期

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

1 李彩虹;李廉;章超;孫守卿;吳孝軍;陳波;;硬件系統(tǒng)SystemC~(FL)模型的SPIN驗(yàn)證[A];2006年全國(guó)理論計(jì)算機(jī)科學(xué)學(xué)術(shù)年會(huì)論文集[C];2006年

相關(guān)重要報(bào)紙文章 前1條

1 本報(bào)記者 邊歆;異常檢測(cè)是阻止蠕蟲攻擊的最好方法？[N];網(wǎng)絡(luò)世界;2006年

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

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

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

3 張君華;實(shí)時(shí)隨機(jī)系統(tǒng)的分析診斷與控制研究[D];南京航空航天大學(xué);2011年

4 高妍妍;ASIP體系結(jié)構(gòu)形式化建模與驗(yàn)證方法研究[D];中國(guó)科學(xué)技術(shù)大學(xué);2009年

5 萬良;基于行為時(shí)序邏輯TLA的系統(tǒng)、規(guī)則與協(xié)議檢測(cè)的研究[D];貴州大學(xué);2009年

6 呂鳴松;實(shí)時(shí)系統(tǒng)最壞情況執(zhí)行時(shí)間分析技術(shù)的研究[D];東北大學(xué);2010年

7 呂正;多核處理器存儲(chǔ)系統(tǒng)的驗(yàn)證方法研究[D];西北大學(xué);2013年

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

1 汪永虎;基于內(nèi)存和狀態(tài)管理的模型檢測(cè)方法[D];電子科技大學(xué);2012年

2 安鑫;面向一類基于輪數(shù)的分布式算法的狀態(tài)空間分析與模型檢測(cè)[D];山東大學(xué);2010年

3 國(guó)瑩;基于共享總線的多核實(shí)時(shí)系統(tǒng)WCET分析[D];東北大學(xué);2010年

4 周懷洋;多核系統(tǒng)上的調(diào)度策略建模與分析[D];上海交通大學(xué);2011年

5 張鵬;Linux環(huán)境下基于MSVL的仿真與驗(yàn)證[D];西安電子科技大學(xué);2013年

6 陳衛(wèi)濤;動(dòng)態(tài)可重構(gòu)系統(tǒng)形式化驗(yàn)證工具與原型平臺(tái)的設(shè)計(jì)與實(shí)現(xiàn)[D];東北大學(xué);2010年

7 易良辰;普適環(huán)境下基于抽象狀態(tài)機(jī)的服務(wù)組合的分析與驗(yàn)證[D];上海交通大學(xué);2013年

8 李亞利;基于可能性測(cè)度的時(shí)序邏輯性質(zhì)研究[D];陜西師范大學(xué);2013年

9 鄧輝;基于可能性測(cè)度的計(jì)算樹邏輯與可能性互模擬[D];陜西師范大學(xué);2013年

，

本文編號(hào)：1483189