發(fā)布時(shí)間：2018-10-23 10:11

【摘要】：提出一種基于模型檢測(cè)工具SPIN的LTL屬性分解方法以解決狀態(tài)空間爆炸問題。根據(jù)邏輯和時(shí)序操作符常見的組合情況,討論不同的屬性分解模式,根據(jù)子屬性構(gòu)建的切片準(zhǔn)則進(jìn)行程序切片,利用SPIN對(duì)切片后的等價(jià)簡化模型進(jìn)行檢測(cè),從而將對(duì)原模型上屬性的檢測(cè)轉(zhuǎn)化成對(duì)復(fù)雜度較低的子模型上各子屬性的分別檢測(cè)。實(shí)驗(yàn)結(jié)果表明,該方法具有一定的有效性。
[Abstract]:A LTL attribute decomposition method based on model checking tool SPIN is proposed to solve the problem of state space explosion. According to the common combination of logic and sequential operators, different attribute decomposition modes are discussed. The program slicing is carried out according to the slicing criterion constructed by subattributes, and the equivalent simplified model after slicing is detected by SPIN. Thus, the detection of attributes on the original model is transformed into the detection of each subattribute on the submodel with lower complexity. Experimental results show that the method is effective.
【作者單位】： 南京大學(xué)計(jì)算機(jī)軟件新技術(shù)國家重點(diǎn)實(shí)驗(yàn)室;南京大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)系;
【基金】：國家自然科學(xué)基金項(xiàng)目(61170070) 國家科技支撐計(jì)劃項(xiàng)目(2012BAK26B01) 國家高技術(shù)研究發(fā)展計(jì)劃項(xiàng)目(2011AA1A202)
【分類號(hào)】：TP306

【參考文獻(xiàn)】

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

1 李興鋒;張新常;楊美紅;閻保平;;基于SPIN的模塊化模型檢測(cè)方法研究[J];電子與信息學(xué)報(bào);2011年04期

2 戎玫;何志學(xué);張廣泉;;一種基于LTL性質(zhì)的面向?qū)ο蟛l(fā)程序切片方法[J];計(jì)算機(jī)應(yīng)用;2008年05期

【共引文獻(xiàn)】

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

1 高洪博;李清寶;王煒;朱瑜;;基于敏感位置識(shí)別的狀態(tài)化簡技術(shù)研究[J];電子與信息學(xué)報(bào);2013年03期

2 錢成;燕雪峰;周勇;徐海生;;基于狀態(tài)約簡的順序圖和狀態(tài)圖一致性檢測(cè)[J];計(jì)算機(jī)應(yīng)用研究;2014年05期

3 王曦;徐中偉;;基于啟發(fā)式NDFS的模型檢測(cè)新算法[J];小型微型計(jì)算機(jī)系統(tǒng);2012年08期

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

1 高洪博;指令誘發(fā)型硬件木馬檢測(cè)技術(shù)研究[D];解放軍信息工程大學(xué);2013年

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

1 秦英;VoIP數(shù)據(jù)流的可信傳輸及其安全屬性的形式化驗(yàn)證[D];北京交通大學(xué);2013年

【二級(jí)參考文獻(xiàn)】

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

1 董威,王戟,齊治昌;并發(fā)程序的切片模型檢驗(yàn)方法[J];計(jì)算機(jī)學(xué)報(bào);2003年03期

【相似文獻(xiàn)】

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

1 曾云輝;朱光慧;;基于屬性分解的信息安全風(fēng)險(xiǎn)分析與計(jì)算模型[J];山東科學(xué);2009年02期

2 余永紅;柏文陽;;強(qiáng)制數(shù)據(jù)隱私和用戶隱私的外包數(shù)據(jù)庫服務(wù)研究[J];計(jì)算機(jī)應(yīng)用研究;2011年01期

3 ;[J];;年期

4 ;[J];;年期

5 ;[J];;年期

6 ;[J];;年期

7 ;[J];;年期

8 ;[J];;年期

9 ;[J];;年期

10 ;[J];;年期

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

1 楊剛;外包數(shù)據(jù)庫機(jī)密性保護(hù)技術(shù)研究[D];解放軍信息工程大學(xué);2013年

，

本文編號(hào)：2288922