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

Bisimulation equivalence for polynomial program model

作　　者：邓辉[1] 吴尽昭[1,2] 

机构地区：[1]北京交通大学计算机与信息技术学院,北京100044 [2]广西民族大学,广西530006

出　　处：《北京交通大学学报》2011年第5期73-77,88,共6页JOURNAL OF BEIJING JIAOTONG UNIVERSITY

基　　金：国家自然科学基金资助项目(60973147;60873118);教育部博士点基金项目资助(20090009110006)

摘　　要：针对程序的行为等价性,提出多项式程序模型的互模拟等价,适用于代数程序模型描述的软件系统设计和验证分析.给出多项式程序模型互模拟等价概念,建立互模拟等价的符号计算方法,选取结构简单的模型,简化程序设计,缓解状态爆炸导致的形式化验证方法计算复杂度过高而难于实现的问题.最后给出并发程序的相关实例.In allusion to the equivalence for behavior of program, the paper proposes bisimulation equivalence for polynomial program model. Bisimulation equivalence suits for software system design and verification which are described by algebraic program model. The paper defines the notion of bisimula- tion equivalence for polynomial program model, instaurates a symbolic calculation method for bisimula- tion equivalence, and selects a simple model to simplify procedure. It can also effectively alleviate the problem of formal verification method caused by state explosion that the computational procedure is too complex to implement. Finally, an example of the concurrent program is shown.

关 键 词：互模拟等价 多项式程序模型 非确定性 并发 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]