多项式程序模型的互模拟等价

《多项式程序模型的互模拟等价》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、第35卷第5期北京交通大学学报Vl01．35No．42011年10月oI爪NAL0FBE1．1INGUA(爪)NGUNIVERSITYOct．2011文章编号：1673—0291(2011)05—0073—05多项式程序模型的互模拟等价邓辉’，吴尽昭，2(1．北京交通大学计算机与信息技术学院，北京100044；2．广西民族大学，广西530006)摘要：针对程序的行为等价性，提出多项式程序模型的互模拟等价，适用于代数程序模型描述的软件系统设计和验证分析．给出多项式程序模型互模拟等价概念，建立互模拟等价的符号计算方法，选取结构简单的模型，简化程序设计，缓

2、解状态爆炸导致的形式化验证方法计算复杂度过高而难于实现的问题．最后给出并发程序的相关实例．关键词：互模拟等价；多项式程序模型；非确定性；并发中图分类号：TP301文献标志码：ABisimulationequivalenceforpolynomialprogrammodelDENGHui．WUJinzhao，(1．SchoolofComputerandInformationTechnology，BeijingJiaotongUniversity，Beijing100044，China；2．GuangxiUniversityforNationalitie

3、s，Guangxi530006，China)Abstract：Inallusiontotheequivalenceforbehaviorofprogram，thepaperproposesbisimulationequiv—alenceforpolynomialprogrammode1．Bisimulationequivalencesuitsforsoftwaresystemdesignandverificationwhicharedescribedbyalgebraicprogrammode1．Thepaperdefinesthenotionofb

4、isimula—tionequivalenceforpolynomialprogrammodel，instauratesasymboliccalculationmethodforbisimula—tionequivalence，andselectsasimplemodeltosimplifyprocedure．Itcanalsoeffectivelyalleviatetheproblemofformalverificationmethodcausedbystateexplosionthatthecomputationalprocedureistooc

5、omplextoimplement．Finally，anexampleoftheconcurrentprogramisshown．Keywords：bisimulationequivalence；nondeterminism；polynomialprogrammodel；concurrency随着软件系统复杂度的不断增长，程序设计和的程序模型，侧重模型的动态行为特征，人们建立了验证面临很大的挑战，软件开发必须保证软件的正不同的模型行为等价关系．行为等价关系大体上分确性和可靠性，最终得到简单的程序模型l1J，提高为两种：线性与分支时间等价．这些等价之间

6、粗糙程设计及验证的效率．在软件系统设计与验证分析领度的比较关系，称为等价谱系，例如1990年，R．J．域中，一个主要问题是如何定义和判定程序的行为vanG1abbeek成功建立了线性和分支时间的等价谱等价．2003年，Z．Manna等人定义以多项式等式数系J．M．Hennessy等人定义的测试／失败等价，以据流表示状态转移标记的混杂系统程序模型，并首及D．M．R．Park定义的互模拟等价，后者被R．Mil．次建立基于多项式Groebner理论的程序不变量的ner成功地应用于著名的进程代数CCS．在等价谱计算方法_2l，创建了基于多项式代数程序设计与验

7、系中，互模拟等价是一种定义在状态空间等价和状证分析的新途径．态空间约简上的等价语义，在进程代数和模型检在等价关系方面，早在1990年之前，对于离散测_4j理论中具有重要意义．进程代数用一组算子作收稿日期：2010—0902基金项目：国家自然科学基金资助项目(60973147，60873118)；教育部博士点基金项目资助(2009oo09110006)作者简介：邓辉(1985一)，女，湖北孝感人，博士生，研究方向为形式化方法，自动推理，验证技术．email：denghui73@126．tom吴尽昭(1966一)，男，黑龙江齐齐哈尔人，研究员，博士生导师

8、．email：himrwujz@yaheo．com．cn．74北京交通大学学报第35卷为进程的构件，其核心问