摘要
针对任务关键性的武器装备控制领域,选用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.
出处
《计算机工程与设计》
CSCD
北大核心
2005年第12期3295-3297,3300,共4页
Computer Engineering and Design
关键词
B方法
形式化方法
弹道计算机
抽象机
不变式
B-method
formal methods
ballistic computer
abstract machine
invariants
