形式化方法B的精化  

Refinement in Formal Method B

作　　者：高洪江[1] 覃征[1] 鹿蕾[2] 邵利平[1] 

机构地区：[1]西安交通大学电子与信息工程学院 [2]鲁东大学图书馆,烟台264025

出　　处：《计算机工程》2007年第9期49-51,共3页Computer Engineering

基　　金：国家"973"计划基金资助项目(2004CB719401);国家自然科学基金资助项目(60542004)

摘　　要：形式化方法B支持从抽象规约到实现的完整的开发过程,用于开发安全关键的软件系统。给出了B方法精化的定义后,介绍了抽象机的精化过程与方法,结合实例分析了仅使用前向精化的普通精化规则的不完整性,通过引入反向精化提供了完备的精化理论,二者联合起来能够证明任何正确的精化。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.

关 键 词：形式化方法 广义代换 抽象机 前向精化 反向精化 证明义务 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]