本文關(guān)鍵詞： 異步通信程序 通信Petri網(wǎng) 可覆蓋性 程序驗證 k-型　出處：《軟件學(xué)報》2017年04期 　論文類型：期刊論文

【摘要】：由于多棧的模型圖靈等價,因此,通用的異步通信程序模型的驗證問題不可判定.為此,基于Petri網(wǎng),提出了一個新的模型通信——通信Petri網(wǎng),對異步通信程序進行刻畫.通過對輸入通信進行k-型限制以及對每個棧進行基于正則語言泵引理的抽象,通過將這樣限制下的模型編碼到數(shù)據(jù)Petri網(wǎng),證明了限制下的新模型可覆蓋性可判定.
[Abstract]:Because the multi-stack model Turing is equivalent, the verification problem of the universal asynchronous communication program model can not be determined. Therefore, based on Petri net, a new model communication-communication Petri net is proposed. This paper describes the asynchronous communication program. By limiting the input communication to k- type and abstracting each stack based on the regular language pump Lemma, the model under this limitation is encoded into the data Petri net. It is proved that the coverage of the new model is determinable.
【作者單位】： 上海交通大學(xué)軟件學(xué)院;
【基金】：國家自然科學(xué)基金(61672340,61472238,91318301)~~
【分類號】：TP311.1;TP301.1
【正文快照】： 隨著大規(guī)模復(fù)雜多核系統(tǒng)的廣泛使用,并發(fā)程序得到了越來越多的應(yīng)用.但并發(fā)程序不同于順序程序具有通用的程序驗證模型(下推系統(tǒng)),即使將所有數(shù)據(jù)域抽象成有限域,并發(fā)程序所對應(yīng)的多棧模型也圖靈等價,其上最簡單的驗證,如可達性不可判定[1].異步程序是并發(fā)程序中最常用的管理并

【相似文獻】

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

1 丁偉，顧冠群;基于異步通信機制的群通信服務(wù)[J];電信科學(xué);1994年09期

2 楊秀合;異步通信協(xié)議及控制規(guī)程設(shè)計實例[J];計算機系統(tǒng)應(yīng)用;1994年08期

3 周凱;;Signalman Error-Free異步通信輔助裝置[J];通信技術(shù);1986年02期

4 沈湘衡;;一種主從被動式異步通信接口[J];微型機與應(yīng)用;1984年02期

5 劉振宇,陳禾,韓月秋;新型波前陣列握手電路(英文)[J];Journal of Beijing Institute of Technology(English Edition);2001年02期

6 李阜,陳小歐;Windows環(huán)境下的串口異步通信程序設(shè)計[J];電子技術(shù)應(yīng)用;1997年02期

7 李阜,陳小歐;Windows環(huán)境的串口異步通信程序設(shè)計[J];計算機系統(tǒng)應(yīng)用;1997年02期

8 張曉華;;使用異步通信組件構(gòu)筑松散耦合系統(tǒng)[J];武漢船舶職業(yè)技術(shù)學(xué)院學(xué)報;2006年03期

9 簡林莎;李驪;任淑加;;提高異步通信傳輸速率的方法[J];電測與儀表;1997年02期

10 胡延平,李廣森;TMS320C54X軟件模擬實現(xiàn)UART技術(shù)[J];微處理機;2000年03期

相關(guān)會議論文 前5條

1 王芳瀟;;一種基于異步通信機制的輕量級數(shù)據(jù)校驗?zāi)Ｐ偷难芯縖A];2009系統(tǒng)仿真技術(shù)及其應(yīng)用學(xué)術(shù)會議論文集[C];2009年

2 何敏;聶典;劉榮;龔晶;;異步通信串行電路的建模及仿真[A];2008中國儀器儀表與測控技術(shù)進展大會論文集（Ⅲ）[C];2008年

3 朱正平;;基于C54X-DSP的軟件UART的實現(xiàn)[A];中國地球物理學(xué)會年刊2002——中國地球物理學(xué)會第十八屆年會論文集[C];2002年

4 殷松;;基于RSLinx OPC的VB與PLC異步通信的實現(xiàn)[A];全國冶金自動化信息網(wǎng)2012年年會論文集[C];2012年

5 李耀華;;基于Webparts個性化和Ajax無刷新技術(shù)的電子商務(wù)網(wǎng)的設(shè)計與實現(xiàn)[A];第二十六屆中國（天津）2012IT、網(wǎng)絡(luò)、信息技術(shù)、電子、儀器儀表創(chuàng)新學(xué)術(shù)會議論文集[C];2012年

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

1 張小西;WS-I：統(tǒng)一標準,助推SOA[N];網(wǎng)絡(luò)世界;2006年

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

1 張志偉;面向?qū)ο螽惒酵ㄐ胖虚g件的研究與實現(xiàn)[D];國防科學(xué)技術(shù)大學(xué);2004年

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

1 許立波;面向網(wǎng)絡(luò)化制造的分布式異步通信的研究[D];江蘇大學(xué);2003年

2 冷國標;異步通信技術(shù)的環(huán)境監(jiān)測軟件系統(tǒng)的設(shè)計與實現(xiàn)[D];吉林大學(xué);2012年

3 莫大鵬;MSVL中異步通信方法的研究與實現(xiàn)[D];西安電子科技大學(xué);2012年

4 侯志強;GSRP：一種支持異步通信的應(yīng)用協(xié)議[D];中國科學(xué)院研究生院（計算技術(shù)研究所）;2004年

5 葉雙;基于CORBA的非耦合異步通信技術(shù)的理論研究及其在Trobus系統(tǒng)上的應(yīng)用[D];福州大學(xué);2003年

6 董鑫;基于AJAX的動態(tài)Web開發(fā)技術(shù)探討[D];河南大學(xué);2007年

7 戴振;基于B/S模型的虛[D];華中科技大學(xué);2011年

8 楊振國;客戶機—服務(wù)器交互模式類型系統(tǒng)的演進特性研究[D];浙江師范大學(xué);2013年

，

本文編號：1446112