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

【摘要】：CSP(Communicating Sequential Processes)是構建并發(fā)系統(tǒng)和網(wǎng)絡安全協(xié)議的經(jīng)典方法。當前主流的CSP模型驗證方法需將進程轉化為遷移系統(tǒng),轉化過程比較復雜;性質采用跡進行規(guī)范,不利于活性的描述。提出了一種基于進程跡的CSP模型驗證框架,其性質采用通用的規(guī)范方法LTL進行描述。利用ASP(Answer Set Programming)技術實現(xiàn)了一個CSP驗證系統(tǒng)。實驗表明,與類似系統(tǒng)相比,該系統(tǒng)的描述能力更強,驗證結果的準確性更高,在性質不滿足時還可提供反例。
[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.
【作者單位】： 桂林電子科技大學計算機科學與工程學院;
【基金】：國家自然科學基金(61262008,61063002) 廣西自然基金(2011GXNSFA018166,2011GXNSFA018164) 廣西可信軟件重點實驗室基金(kx201113)資助
【分類號】：TP393.08

【參考文獻】

相關期刊論文 前1條

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

【共引文獻】

相關期刊論文 前10條

1 李仲俠;通信業(yè)務自然描述方法的研究[J];長春郵電學院學報;1997年03期

2 趙波，李文;C程序遞歸變換預編譯系統(tǒng)的設計[J];大連鐵道學院學報;1996年01期

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

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

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

6 林添榮;蔣建民;;UML活動圖的一種邏輯語義[J];福建師范大學學報(自然科學版);2010年03期

7 劉富春;方程邏輯Institution理論及其性質[J];廣東有色金屬學報;2005年01期

8 李侃，王兵山，，李舟軍;并發(fā)面向對象語言的演算語義研究[J];國防科技大學學報;1996年01期

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

10 白金山;杜習慧;趙莉莉;李祥;;并發(fā)程序驗證器CPV的設計與應用研究[J];貴州大學學報(自然科學版);2008年01期

相關會議論文 前2條

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

2 姚丹霖;殷建平;;大型漢英雙語電子詞典的結構與自動生成[A];數(shù)據(jù)庫研究進展97——第十四屆全國數(shù)據(jù)庫學術會議論文集（下）[C];1997年

相關博士學位論文 前10條

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

2 代飛;基于EPMM的軟件演化過程模型驗證[D];云南大學;2011年

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

4 曾穎;基于抽象解釋的軟件保護相關問題研究[D];解放軍信息工程大學;2011年

5 郭健強;面向對象軟件測試理論與技術的研究[D];西安電子科技大學;1999年

6 李廣元;LTLC：面向實時與混成系統(tǒng)的連續(xù)時序邏輯[D];中國科學院軟件研究所;2001年

7 艾萍;構件柔性組裝描述的形式化方法研究及其在水利領域的應用[D];河海大學;2002年

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

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

10 徐曉泉;完備格的關系表示理論及其應用[D];四川大學;2004年

相關碩士學位論文 前10條

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

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

3 李超;基于擴展下推自動機的Java程序安全相關行為模型自動生成[D];東北師范大學;2011年

4 費利明;基于JVMTI實現(xiàn)安全策略的強制實施[D];東北師范大學;2011年

5 鄭建丹;基于組件的逐步求精程序設計方法[D];中國科學院軟件研究所;2001年

6 孫曉舟;HLR設計方法研究[D];西安電子科技大學;2002年

7 寧愛兵;面向事實程序設計的構思[D];江西師范大學;2003年

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

9 王振;MSC前臺進程對象化方法研究[D];南京理工大學;2004年

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

【二級參考文獻】

相關期刊論文 前1條

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

【相似文獻】

相關期刊論文 前10條

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

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

3 李海鷹,程灝,葉為全,莊鎮(zhèn)泉;基于協(xié)同偵測技術的移動主體模型驗證策略研究[J];計算機學報;2005年05期

4 袁勇福;高春鳴;劉榮勝;;Web服務組合的互模擬驗證[J];計算機應用;2006年10期

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

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

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

8 周昆;金可音;;一種Web服務組合形式化模型及驗證方法[J];微計算機信息;2010年30期

9 劉一靜;謝鴻波;吳遠成;;安全協(xié)議認證屬性的設計框架研究[J];計算機應用;2007年12期

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

相關會議論文 前7條

1 張宇;方濱興;張宏莉;;Internet拓撲演化機理驗證[A];2008通信理論與技術新發(fā)展——第十三屆全國青年通信學術會議論文集（下）[C];2008年

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

3 李磊;譚慶平;;Web服務兼容性及其驗證算法[A];中國通信學會第六屆學術年會論文集（上）[C];2009年

4 文靜華;張梅;張煥國;;電子支付協(xié)議的博弈邏輯模型與形式化分析[A];2007年全國開放式分布與并行計算機學術會議論文集(上冊)[C];2007年

5 王美姣;錢彥軍;姚紹文;余正祥;;服務組合語言在SOA中的應用[A];云南省機械工程學會2010年年會論文集[C];2010年

6 吳亮;袁兆山;;基于模糊Petri網(wǎng)的語義Web服務組合[A];全國第20屆計算機技術與應用學術會議（CACIS·2009）暨全國第1屆安全關鍵技術與應用學術會議論文集（上冊）[C];2009年

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

相關重要報紙文章 前1條

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

相關博士學位論文 前7條

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

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

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

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

5 包力;Web服務組合形式化建模與驗證研究[D];大連海事大學;2009年

6 胡佳;語義Web服務自動組合及驗證的研究[D];天津大學;2010年

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

相關碩士學位論文 前10條

1 張健;MMORPG服務器關鍵技術研究[D];浙江大學;2006年

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

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

4 盧建軍;Web服務自動遷移[D];北京郵電大學;2006年

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

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

7 吳錚;基于Pi演算的SOAP安全性分析與驗證[D];中國石油大學;2008年

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

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

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

本文編號：2017156