基于通信Petri网的异步通信程序验证模型

发布时间：2018-01-20 00:26

  本文关键词： 异步通信程序 通信Petri网 可覆盖性 程序验证 k-型　出处：《软件学报》2017年04期 　论文类型：期刊论文

【摘要】：由于多栈的模型图灵等价,因此,通用的异步通信程序模型的验证问题不可判定.为此,基于Petri网,提出了一个新的模型通信——通信Petri网,对异步通信程序进行刻画.通过对输入通信进行k-型限制以及对每个栈进行基于正则语言泵引理的抽象,通过将这样限制下的模型编码到数据Petri网,证明了限制下的新模型可覆盖性可判定.
[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.
【作者单位】： 上海交通大学软件学院;
【基金】：国家自然科学基金(61672340,61472238,91318301)~~
【分类号】：TP311.1;TP301.1
【正文快照】： 随着大规模复杂多核系统的广泛使用,并发程序得到了越来越多的应用.但并发程序不同于顺序程序具有通用的程序验证模型(下推系统),即使将所有数据域抽象成有限域,并发程序所对应的多栈模型也图灵等价,其上最简单的验证,如可达性不可判定[1].异步程序是并发程序中最常用的管理并

【相似文献】

相关期刊论文 前10条

1 丁伟，顾冠群;基于异步通信机制的群通信服务[J];电信科学;1994年09期

2 杨秀合;异步通信协议及控制规程设计实例[J];计算机系统应用;1994年08期

3 周凯;;Signalman Error-Free异步通信辅助装置[J];通信技术;1986年02期

4 沈湘衡;;一种主从被动式异步通信接口[J];微型机与应用;1984年02期

5 刘振宇,陈禾,韩月秋;新型波前阵列握手电路(英文)[J];Journal of Beijing Institute of Technology(English Edition);2001年02期

6 李阜,陈小欧;Windows环境下的串口异步通信程序设计[J];电子技术应用;1997年02期

7 李阜,陈小欧;Windows环境的串口异步通信程序设计[J];计算机系统应用;1997年02期

8 张晓华;;使用异步通信组件构筑松散耦合系统[J];武汉船舶职业技术学院学报;2006年03期

9 简林莎;李骊;任淑加;;提高异步通信传输速率的方法[J];电测与仪表;1997年02期

10 胡延平,李广森;TMS320C54X软件模拟实现UART技术[J];微处理机;2000年03期

相关会议论文 前5条

1 王芳潇;;一种基于异步通信机制的轻量级数据校验模型的研究[A];2009系统仿真技术及其应用学术会议论文集[C];2009年

2 何敏;聂典;刘荣;龚晶;;异步通信串行电路的建模及仿真[A];2008中国仪器仪表与测控技术进展大会论文集（Ⅲ）[C];2008年

3 朱正平;;基于C54X-DSP的软件UART的实现[A];中国地球物理学会年刊2002——中国地球物理学会第十八届年会论文集[C];2002年

4 殷松;;基于RSLinx OPC的VB与PLC异步通信的实现[A];全国冶金自动化信息网2012年年会论文集[C];2012年

5 李耀华;;基于Webparts个性化和Ajax无刷新技术的电子商务网的设计与实现[A];第二十六届中国（天津）2012IT、网络、信息技术、电子、仪器仪表创新学术会议论文集[C];2012年

相关重要报纸文章 前1条

1 张小西;WS-I：统一标准,助推SOA[N];网络世界;2006年

相关博士学位论文 前1条

1 张志伟;面向对象异步通信中间件的研究与实现[D];国防科学技术大学;2004年

相关硕士学位论文 前8条

1 许立波;面向网络化制造的分布式异步通信的研究[D];江苏大学;2003年

2 冷国标;异步通信技术的环境监测软件系统的设计与实现[D];吉林大学;2012年

3 莫大鹏;MSVL中异步通信方法的研究与实现[D];西安电子科技大学;2012年

4 侯志强;GSRP：一种支持异步通信的应用协议[D];中国科学院研究生院（计算技术研究所）;2004年

5 叶双;基于CORBA的非耦合异步通信技术的理论研究及其在Trobus系统上的应用[D];福州大学;2003年

6 董鑫;基于AJAX的动态Web开发技术探讨[D];河南大学;2007年

7 戴振;基于B/S模型的虚[D];华中科技大学;2011年

8 杨振国;客户机—服务器交互模式类型系统的演进特性研究[D];浙江师范大学;2013年

，

本文编号：1446112