|
|||||
|
|
| 形式化方法B的精化 | |
| 引用本文： | 高洪江,覃征,鹿蕾,邵利平.形式化方法B的精化[J].计算机工程,2007,33(9):49-51. |
| 作者姓名： | 高洪江 覃征 鹿蕾 邵利平 |
| 作者单位： | 1. 西安交通大学电子与信息工程学院,西安710049;鲁东大学计算机科学与技术学院,烟台264025 2. 西安交通大学电子与信息工程学院,西安710049;清华大学软件学院,北京100084 3. 鲁东大学图书馆,烟台264025 4. 西安交通大学电子与信息工程学院,西安710049 |
| 基金项目： | 国家重点基础研究发展计划(973计划) , 国家自然科学基金 |
| 摘 要： | 形式化方法B支持从抽象规约到实现的完整的开发过程，用于开发安全关键的软件系统。给出了B方法精化的定义后，介绍了抽象机的精化过程与方法，结合实例分析了仅使用前向精化的普通精化规则的不完整性，通过引入反向精化提供了完备的精化理论，二者联合起来能够证明任何正确的精化。 |
| 关 键 词： | 形式化方法 广义代换 抽象机 前向精化 反向精化 证明义务 |
| 文章编号： | 1000-3428（2007）09-0049-03 |
| 修稿时间： | 2006-06-19 |
Refinement in Formal Method B |
|
| GAO Hongjiang,QIN Zheng,LU Lei,SHAO Liping.Refinement in Formal Method B[J].Computer Engineering,2007,33(9):49-51. | |
| Authors: | GAO Hongjiang QIN Zheng LU Lei SHAO Liping |
| Affiliation: | (1. School of Electronics and Information Engineering, Xi’an Jiaotong University, Xi’an 710049; 2. School of Computer Science and Technology, Ludong University, Yantai 264025; 3. School of Software, Tsinghua University, Beijing 100084; 4. Library, Ludong University, Yantai 264025) |
| Abstract: | Formal method B supports the whole development from abstract specifications to implementation,which is used to develop safety-critical systems in software.This paper presents the definition of refinement in B and describes the refinement process of abstract machine and its approaches.After illuminating via an example that B's ordinary refinement rules only in terms of forward refinement are incomplete,backward refinement is introduced to endow B for the first time with two tractable and jointly complete refinement theories which together are sufficient for proving any valid refinement. |
| Keywords: | Formal method Generalized substitution Abstract machine Forward refinement Backward refinement Proof obligations |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |
| 点击此处可从《计算机工程》浏览原始摘要信息 | |
| 点击此处可从《计算机工程》下载全文 | |