General-Service Ballistic Computer Programming Based on B-Method

摘要

Formal methods offer the promise of significant improvement on quality and reliability of critical embedded software. B-Method is employed to develop general-service ballistic computer programs in the paper, each of which can be adapted to a family of service/weapon-specific ballistic computers. Based on the structuring mechanisms of B-method, a unified approach is proposed to systematically control the complexity of ballistic parameters in the process of type and operation refinement, and ultimately a series of high reliable, reusable, and scalable programs are produced. Experiences with the application of the method and tools are also discussed.