基于B方法的弹道计算机程序设计技术  

B-method based approach for designing ballistic computers

作　　者：张子丘 郑宇军[2] 李海英 

机构地区：[1]武器装备论证研究中心,北京100034 [2]中国科学院软件研究所,北京100080 [3]工程装备系统工程研究所,北京100093

出　　处：《计算机工程与设计》2005年第12期3295-3297,3300,共4页Computer Engineering and Design

摘　　要：针对任务关键性的武器装备控制领域,选用B方法来设计通用弹道计算机程序,显著地提高了软件的质量和可靠性。在开发过程中,利用抽象机机制对基本弹道计算机进行建模,并通过逐步精化的方法扩展弹道计算机功能,从而有效地控制了弹道计算参数之间的复杂关系,依赖不变式技术形式化地保证了软件运行时的安全性,并使得生成的程序具有良好的重用性和可扩展性。The B-method to design general ballistic computer programs was selected, which represented a typical application in mission critical areas where formal methods were increasingly applied to improve software quality and reliability. By modeling each basic ballistic computer as an abstract machine and stepwise enhancing new functions into existing machines during the refinement process, the complexity between ballistic parameters was well controlled and reduced, the run-time security of software was formally guaranteed in virtue of invariants, and the programs with reusability and extensibility were ultimately generated.

关 键 词：B方法 形式化方法 弹道计算机 抽象机 不变式 

分 类 号：TP391.8[自动化与计算机技术—计算机应用技术]