發(fā)布時(shí)間：2018-06-14 11:01

  本文選題：通信順序進(jìn)程(CSP) + 并發(fā)系統(tǒng)�。� 參考：《計(jì)算機(jī)科學(xué)》2013年11期

【摘要】：CSP(Communicating Sequential Processes)是構(gòu)建并發(fā)系統(tǒng)和網(wǎng)絡(luò)安全協(xié)議的經(jīng)典方法。當(dāng)前主流的CSP模型驗(yàn)證方法需將進(jìn)程轉(zhuǎn)化為遷移系統(tǒng),轉(zhuǎn)化過(guò)程比較復(fù)雜;性質(zhì)采用跡進(jìn)行規(guī)范,不利于活性的描述。提出了一種基于進(jìn)程跡的CSP模型驗(yàn)證框架,其性質(zhì)采用通用的規(guī)范方法LTL進(jìn)行描述。利用ASP(Answer Set Programming)技術(shù)實(shí)現(xiàn)了一個(gè)CSP驗(yàn)證系統(tǒng)。實(shí)驗(yàn)表明,與類似系統(tǒng)相比,該系統(tǒng)的描述能力更強(qiáng),驗(yàn)證結(jié)果的準(zhǔn)確性更高,在性質(zhì)不滿足時(shí)還可提供反例。
[Abstract]:CSP Communication process is a classic method for building concurrent systems and network security protocols. The current mainstream CSP model verification methods need to transform the process into a migration system, the transformation process is more complex, and the properties of CSP model are standardized, which is not conducive to the description of activity. A CSP model verification framework based on process trace is proposed. Its properties are described by the universal specification method LTL. A CSP verification system is implemented by using the ASPU Answer set programming technology. The experimental results show that the proposed system has better description ability and higher accuracy than similar systems, and can provide counterexample when its properties are not satisfied.
【作者單位】： 桂林電子科技大學(xué)計(jì)算機(jī)科學(xué)與工程學(xué)院;
【基金】：國(guó)家自然科學(xué)基金(61262008,61063002) 廣西自然基金(2011GXNSFA018166,2011GXNSFA018164) 廣西可信軟件重點(diǎn)實(shí)驗(yàn)室基金(kx201113)資助
【分類號(hào)】：TP393.08

【參考文獻(xiàn)】

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

1 趙嶺忠;張超;錢俊彥;;基于ASP的CSP并發(fā)系統(tǒng)驗(yàn)證研究[J];計(jì)算機(jī)科學(xué);2012年12期

【共引文獻(xiàn)】

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

1 李仲俠;通信業(yè)務(wù)自然描述方法的研究[J];長(zhǎng)春郵電學(xué)院學(xué)報(bào);1997年03期

2 趙波，李文;C程序遞歸變換預(yù)編譯系統(tǒng)的設(shè)計(jì)[J];大連鐵道學(xué)院學(xué)報(bào);1996年01期

3 李文，朱力鳴;分層遞階智能控制任務(wù)轉(zhuǎn)換模型的研究現(xiàn)狀[J];大連鐵道學(xué)院學(xué)報(bào);1996年02期

4 劉樹(shù)錕;莫正杰;吳沛林;黃小波;;基于Java建模語(yǔ)言的不變量檢測(cè)工具[J];電腦開(kāi)發(fā)與應(yīng)用;2012年05期

5 張宇;平龍妹;;基于敏捷建模的形式化需求分析方法[J];電腦知識(shí)與技術(shù);2008年34期

6 林添榮;蔣建民;;UML活動(dòng)圖的一種邏輯語(yǔ)義[J];福建師范大學(xué)學(xué)報(bào)(自然科學(xué)版);2010年03期

7 劉富春;方程邏輯Institution理論及其性質(zhì)[J];廣東有色金屬學(xué)報(bào);2005年01期

8 李侃，王兵山，，李舟軍;并發(fā)面向?qū)ο笳Z(yǔ)言的演算語(yǔ)義研究[J];國(guó)防科技大學(xué)學(xué)報(bào);1996年01期

9 王彩芬;程序正確性證明及循環(huán)不變式的尋找方法[J];甘肅科學(xué)學(xué)報(bào);2000年03期

10 白金山;杜習(xí)慧;趙莉莉;李祥;;并發(fā)程序驗(yàn)證器CPV的設(shè)計(jì)與應(yīng)用研究[J];貴州大學(xué)學(xué)報(bào)(自然科學(xué)版);2008年01期

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

1 柳永坡;晏海華;張懋;劉雪梅;;測(cè)試流程管理與監(jiān)控技術(shù)的研究與實(shí)現(xiàn)[A];第五屆中國(guó)測(cè)試學(xué)術(shù)會(huì)議論文集[C];2008年

2 姚丹霖;殷建平;;大型漢英雙語(yǔ)電子詞典的結(jié)構(gòu)與自動(dòng)生成[A];數(shù)據(jù)庫(kù)研究進(jìn)展97——第十四屆全國(guó)數(shù)據(jù)庫(kù)學(xué)術(shù)會(huì)議論文集（下）[C];1997年

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

1 吳新星;基于語(yǔ)言的軟件可信性度量理論及其應(yīng)用[D];華東師范大學(xué);2011年

2 代飛;基于EPMM的軟件演化過(guò)程模型驗(yàn)證[D];云南大學(xué);2011年

3 陳曉江;分布式系統(tǒng)軟件體系結(jié)構(gòu)建模與開(kāi)發(fā)方法研究[D];西北大學(xué);2010年

4 曾穎;基于抽象解釋的軟件保護(hù)相關(guān)問(wèn)題研究[D];解放軍信息工程大學(xué);2011年

5 郭健強(qiáng);面向?qū)ο筌浖䴗y(cè)試?yán)碚撆c技術(shù)的研究[D];西安電子科技大學(xué);1999年

6 李廣元;LTLC：面向?qū)崟r(shí)與混成系統(tǒng)的連續(xù)時(shí)序邏輯[D];中國(guó)科學(xué)院軟件研究所;2001年

7 艾萍;構(gòu)件柔性組裝描述的形式化方法研究及其在水利領(lǐng)域的應(yīng)用[D];河海大學(xué);2002年

8 鄭紅;分布式系統(tǒng)形式化建模技術(shù)研究[D];中國(guó)科學(xué)院研究生院（軟件研究所）;2003年

9 胡瑜;基于有色Petri網(wǎng)理論的并行自動(dòng)測(cè)試系統(tǒng)建模研究[D];電子科技大學(xué);2003年

10 徐曉泉;完備格的關(guān)系表示理論及其應(yīng)用[D];四川大學(xué);2004年

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

1 朱恒亮;SOA中服務(wù)與服務(wù)組合的形式化研究[D];福建師范大學(xué);2010年

2 楊志財(cái);安全策略的形式化描述及其可視化實(shí)現(xiàn)[D];東北師范大學(xué);2011年

3 李超;基于擴(kuò)展下推自動(dòng)機(jī)的Java程序安全相關(guān)行為模型自動(dòng)生成[D];東北師范大學(xué);2011年

4 費(fèi)利明;基于JVMTI實(shí)現(xiàn)安全策略的強(qiáng)制實(shí)施[D];東北師范大學(xué);2011年

5 鄭建丹;基于組件的逐步求精程序設(shè)計(jì)方法[D];中國(guó)科學(xué)院軟件研究所;2001年

6 孫曉舟;HLR設(shè)計(jì)方法研究[D];西安電子科技大學(xué);2002年

7 寧愛(ài)兵;面向事實(shí)程序設(shè)計(jì)的構(gòu)思[D];江西師范大學(xué);2003年

8 吳海濤;對(duì)象并發(fā)演算模型及對(duì)象語(yǔ)言語(yǔ)義研究[D];鄭州大學(xué);2003年

9 王振;MSC前臺(tái)進(jìn)程對(duì)象化方法研究[D];南京理工大學(xué);2004年

10 崔海渤;Java語(yǔ)言的類和多態(tài)性的公理語(yǔ)義[D];大連理工大學(xué);2005年

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

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

1 張兆慶,蔣昌俊,喬如良,葉志寶,周杰;PVM并行程序驗(yàn)證系統(tǒng)的原理與實(shí)現(xiàn)[J];計(jì)算機(jī)學(xué)報(bào);1999年04期

【相似文獻(xiàn)】

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

1 李楊;程建華;房鼎益;陳曉江;馮健;;并發(fā)系統(tǒng)的安全性與活性的驗(yàn)證方法[J];計(jì)算機(jī)工程與應(yīng)用;2008年04期

2 吳丘林;;一種自頂而下的Web-服務(wù)全局行為設(shè)計(jì)方法[J];電腦知識(shí)與技術(shù)(學(xué)術(shù)交流);2007年10期

3 李海鷹,程灝,葉為全,莊鎮(zhèn)泉;基于協(xié)同偵測(cè)技術(shù)的移動(dòng)主體模型驗(yàn)證策略研究[J];計(jì)算機(jī)學(xué)報(bào);2005年05期

4 袁勇福;高春鳴;劉榮勝;;Web服務(wù)組合的互模擬驗(yàn)證[J];計(jì)算機(jī)應(yīng)用;2006年10期

5 蔣昌俊，鄭應(yīng)平，疏松桂;并發(fā)系統(tǒng)建模與分析研究[J];高技術(shù)通訊;1996年06期

6 許可;王躍宣;吳澄;;網(wǎng)格服務(wù)鏈模型的驗(yàn)證分析技術(shù)及應(yīng)用[J];中國(guó)科學(xué)(E輯:信息科學(xué));2007年04期

7 辜希武;盧正鼎;;基于Pi-演算的BPEL4 WS Web服務(wù)組合形式化模型[J];計(jì)算機(jī)科學(xué);2007年03期

8 周昆;金可音;;一種Web服務(wù)組合形式化模型及驗(yàn)證方法[J];微計(jì)算機(jī)信息;2010年30期

9 劉一靜;謝鴻波;吳遠(yuǎn)成;;安全協(xié)議認(rèn)證屬性的設(shè)計(jì)框架研究[J];計(jì)算機(jī)應(yīng)用;2007年12期

10 吉順慧;李必信;周宇;;基于順序圖的Web組合服務(wù)屬性驗(yàn)證[J];東南大學(xué)學(xué)報(bào)(自然科學(xué)版);2011年02期

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

1 張宇;方濱興;張宏莉;;Internet拓?fù)溲莼瘷C(jī)理驗(yàn)證[A];2008通信理論與技術(shù)新發(fā)展——第十三屆全國(guó)青年通信學(xué)術(shù)會(huì)議論文集（下）[C];2008年

2 蔡元沛;邢薇;沙寧;;面向RIA的離線并發(fā)控制的研究[A];黑龍江省計(jì)算機(jī)學(xué)會(huì)2009年學(xué)術(shù)交流年會(huì)論文集[C];2010年

3 李磊;譚慶平;;Web服務(wù)兼容性及其驗(yàn)證算法[A];中國(guó)通信學(xué)會(huì)第六屆學(xué)術(shù)年會(huì)論文集（上）[C];2009年

4 文靜華;張梅;張煥國(guó);;電子支付協(xié)議的博弈邏輯模型與形式化分析[A];2007年全國(guó)開(kāi)放式分布與并行計(jì)算機(jī)學(xué)術(shù)會(huì)議論文集(上冊(cè))[C];2007年

5 王美姣;錢彥軍;姚紹文;余正祥;;服務(wù)組合語(yǔ)言在SOA中的應(yīng)用[A];云南省機(jī)械工程學(xué)會(huì)2010年年會(huì)論文集[C];2010年

6 吳亮;袁兆山;;基于模糊Petri網(wǎng)的語(yǔ)義Web服務(wù)組合[A];全國(guó)第20屆計(jì)算機(jī)技術(shù)與應(yīng)用學(xué)術(shù)會(huì)議（CACIS·2009）暨全國(guó)第1屆安全關(guān)鍵技術(shù)與應(yīng)用學(xué)術(shù)會(huì)議論文集（上冊(cè)）[C];2009年

7 王小梅;李新明;劉東;韓星曄;;基于Petri網(wǎng)的網(wǎng)絡(luò)傳輸協(xié)議建模與性能分析[A];全國(guó)第4屆信號(hào)和智能信息處理與應(yīng)用學(xué)術(shù)會(huì)議論文集[C];2010年

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

1 子文;ADIC StorNext/SAN存儲(chǔ)海量數(shù)據(jù)[N];通信產(chǎn)業(yè)報(bào);2003年

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

1 許可;網(wǎng)格服務(wù)流的狀態(tài)π演算形式化驗(yàn)證技術(shù)研究與應(yīng)用[D];清華大學(xué);2007年

2 龍慧云;基于進(jìn)程代數(shù)的Web服務(wù)數(shù)據(jù)和組合的形式化方法研究[D];貴州大學(xué);2009年

3 王玉英;基于賦時(shí)有色Petri網(wǎng)的Web服務(wù)組合建模驗(yàn)證與測(cè)試技術(shù)研究[D];西安電子科技大學(xué);2012年

4 陳靖;帶實(shí)時(shí)的傳值與移動(dòng)系統(tǒng)研究[D];中國(guó)科學(xué)院研究生院（軟件研究所）;2003年

5 包力;Web服務(wù)組合形式化建模與驗(yàn)證研究[D];大連海事大學(xué);2009年

6 胡佳;語(yǔ)義Web服務(wù)自動(dòng)組合及驗(yàn)證的研究[D];天津大學(xué);2010年

7 吳嫻;基于策略域的分布式訪問(wèn)控制模型[D];蘇州大學(xué);2009年

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

1 張健;MMORPG服務(wù)器關(guān)鍵技術(shù)研究[D];浙江大學(xué);2006年

2 付興尊;基于進(jìn)程代數(shù)的多路訪問(wèn)協(xié)議模型研究與實(shí)現(xiàn)[D];華東師范大學(xué);2010年

3 劉子乾;基于攻擊模式的系統(tǒng)漏洞檢測(cè)工具的設(shè)計(jì)與實(shí)現(xiàn)[D];天津大學(xué);2008年

4 盧建軍;Web服務(wù)自動(dòng)遷移[D];北京郵電大學(xué);2006年

5 劉賢;基于工作流的Web服務(wù)組合建模研究[D];中南大學(xué);2010年

6 朱曉紅;基于狀態(tài)演算的網(wǎng)格服務(wù)自動(dòng)組合技術(shù)研究[D];重慶大學(xué);2006年

7 吳錚;基于Pi演算的SOAP安全性分析與驗(yàn)證[D];中國(guó)石油大學(xué);2008年

8 劉勇;有限PI演算的Petri網(wǎng)語(yǔ)義轉(zhuǎn)換研究[D];吉林大學(xué);2009年

9 張帆;基于異步π-演算的兩階段提交協(xié)議的形式化描述和驗(yàn)證[D];國(guó)防科學(xué)技術(shù)大學(xué);2006年

10 康智輝;基于屬性的層次移動(dòng)IPv6（HMIPv6）協(xié)議的驗(yàn)證[D];內(nèi)蒙古大學(xué);2011年

本文編號(hào)：2017156