|
|||||
|
|
| 基于B方法的弹道计算机程序设计技术 | |
| 引用本文： | 张子丘,郑宇军,李海英.基于B方法的弹道计算机程序设计技术[J].计算机工程与设计,2005,26(12):3295-3297,3300. |
| 作者姓名： | 张子丘 郑宇军 李海英 |
| 作者单位： | 1. 武器装备论证研究中心,北京,100034 2. 中国科学院软件研究所,北京,100080;工程装备系统工程研究所,北京,100093 3. 工程装备系统工程研究所,北京,100093 |
| 摘 要： | 针对任务关键性的武器装备控制领域，选用B方法来设计通用弹道计算机程序，显著地提高了软件的质量和可靠性。在开发过程中，利用抽象机机制对基本弹道计算机进行建模，并通过逐步精化的方法扩展弹道计算机功能，从而有效地控制了弹道计算参数之间的复杂关系，依赖不变式技术形式化地保证了软件运行时的安全性，并使得生成的程序具有良好的重用性和可扩展性。 |
| 关 键 词： | B方法 形式化方法 弹道计算机 抽象机 不变式 |
| 文章编号： | 1000-7024（2005）12-3295-03 |
| 收稿时间： | 2004-11-01 |
| 修稿时间： | 2004-11-01 |
B-method based approach for designing ballistic computers |
|
| ZHANG Zi-qiu,ZHENG Yu-jun,LI Hai-ying.B-method based approach for designing ballistic computers[J].Computer Engineering and Design,2005,26(12):3295-3297,3300. | |
| Authors: | ZHANG Zi-qiu ZHENG Yu-jun LI Hai-ying |
| Affiliation: | 1. Center ofArmamentDemonstrationandResearch, Beijing 100034, China; 2. Institute of Software, CAS, Beijing 100080, China; 3. Systems EngineeringResearchlnstituteofEngineerEquipment, Beijing 100093, China |
| Abstract: | 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. |
| Keywords: | B-method formal methods ballistic computer abstract machine invariants |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |