资源描述：
《基于通信Petri网的异步通信程序验证模型》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。
1、软件学报ISSN1000-9825,CODENRUXUEWE-mail:jos@iscas.ac.cnJournalofSoftware,2017,28(4):804−818[doi:10.13328/j.cnki.jos.005191]http://www.jos.org.cn©中国科学院软件研究所版权所有.Tel:+86-10-62562563∗基于通信Petri网的异步通信程序验证模型杨启哲,李国强(上海交通大学软件学院,上海200240)通信作者:李国强,E-mail:li.g@sjtu.edu.cn摘要:由于多栈的模型图灵等价,因此,通用的异步通信程序模型的验证问题不可判定.为
2、此,基于Petri网,提出了一个新的模型通信——通信Petri网,对异步通信程序进行刻画.通过对输入通信进行k-型限制以及对每个栈进行基于正则语言泵引理的抽象,通过将这样限制下的模型编码到数据Petri网,证明了限制下的新模型可覆盖性可判定.关键词:异步通信程序;通信Petri网;可覆盖性;程序验证;k-型中图法分类号:TP311中文引用格式:杨启哲,李国强.基于通信Petri网的异步通信程序验证模型.软件学报,2017,28(4):804−818.http://www.jos.org.cn/1000-9825/5191.htm英文引用格式:YangQZ,LiGQ.Modelonasyn
3、chronouscommunicationprogramverificationbasedoncommunicatingPetrinets.RuanJianXueBao/JournalofSoftware,2017,28(4):804−818(inChinese).http://www.jos.org.cn/1000-9825/5191.htmModelonAsynchronousCommunicationProgramVerificationBasedonCommunicatingPetriNetsYANGQi-Zhe,LIGuo-Qiang(SchoolofSoftware,Shan
4、ghaiJiaotongUniversity,Shanghai200240,China)Abstract:Sincemulti-stackmodelsaregenerallyTuring-complete,verificationproblemsongeneralmodelsforasynchronouscommunicationprogramsareundecidable.ThispaperproposesanewmodelbasedPetrinet,namedcommunicationPetrinets(C-Petrinets)tomodelasynchronouscommunica
5、tionprograms.Applyingthek-shapedrestrictionontheinputcommunicationsandtheabstractiononeachstackbasedonpoppinglemmaofregularlanguages,thecoverabilityproblemoftherestrictedC-PetrinetisdecidablebyencodingthemodeltodataPetrinets.Keywords:asynchronouscommunicationprogram;communicationPetrinet;coverabi
6、lity;programverification;k-shaped随着大规模复杂多核系统的广泛使用,并发程序得到了越来越多的应用.但并发程序不同于顺序程序具有通用的程序验证模型(下推系统),即使将所有数据域抽象成有限域,并发程序所对应的多栈模型也图灵等价,其[1]上最简单的验证,如可达性不可判定.异步程序是并发程序中最常用的管理并发交互的一种方式,该种程序不需要等待函数调用返回结果,可以直接继续执行,直到程序需要用到调用的返回结果时再去等待函数的调用结果;同步程序则相反,一个同步调用要求程序必须等待至函数调用完成返回结果之后,程序才能继续执行下去.异步通信程序在异步调用之时,允许不同线程
7、之间通过中间存储方式进行通信.这样的程序语言包括Erlang,Scala等,其程序行为更加复杂,难以进行建模和验证.[2]在异步程序验证模型的研究上,Sen和Viswanathan提出了多重集下推系统,只允许在栈空的时候发生通信,并证明了该模型的可覆盖性可判定.这样的模型对于异步通信程序而言过于受到限制,因为一般来说,异步[3]通信程序中的通信发生都不是在栈空的时候.Kochems和Ong提出了异步偏序通信下推系统,并且对其进行∗基
