| 多项式程序模型的互模拟等价 |
| |
| 引用本文： | 邓辉,吴尽昭.多项式程序模型的互模拟等价[J].北方交通大学学报,2011(5):73-77,88. |
| |
| 作者姓名： | 邓辉 吴尽昭 |
| |
| 作者单位： | [1]北京交通大学计算机与信息技术学院,北京100044 [2]广西民族大学,广西530006 |
| |
| 基金项目： | 基金项目：国家自然科学基金资助项目（60973147,60873118）;教育部博士点基金项目资助（20090009110006） |
| |
| 摘 要： | 针对程序的行为等价性，提出多项式程序模型的互模拟等价，适用于代数程序模型描述的软件系统设计和验证分析．给出多项式程序模型互模拟等价概念，建立互模拟等价的符号计算方法，选取结构简单的模型，简化程序设计，缓解状态爆炸导致的形式化验证方法计算复杂度过高而难于实现的问题．最后给出并发程序的相关实例．
|
| 关 键 词： | 互模拟等价 多项式程序模型 非确定性 并发 |
Bisimulation equivalence for polynomial program model |
| |
| DENG Hui,WU Jinzhao.Bisimulation equivalence for polynomial program model[J].Journal of Northern Jiaotong University,2011(5):73-77,88. |
| |
| Authors: | DENG Hui WU Jinzhao |
| |
| Institution: | ( School of Computer and Information Technology, Beijing Jiaotong University, Beijing 100044, China; 2. Guangxi University for Nationalities, Guangxi 530006, China) |
| |
| Abstract: | 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. |
| |
| Keywords: | bisimulation equivalence nondeterminism polynomial program model concurrency |
| 本文献已被 维普 等数据库收录！ |
