B-method based approach for designing ballistic computers
Haiying Li · 2005
The B-method to design general ballisticcomputer programs was selected,which represented a typicalapplication in mission-critical areas where formal methods were increasingly applied to improve software qualityand reliability.By modeling eachbasic ballistic computer as an abstract machine and stepwise enhancing new functions into existing machines during the refinement process,the com-plexity 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.