模型检验在航天测控软件上的应用研究

模型检验是确保程序质量的有效手段,能弥补软件测试的不足。但航天测控软件规模大、输入数据复杂、验证性质不明确等因素极大地阻碍了模型检验的应用。针对航天测控软件,分析了其特点以及对其执行模型检验的困难,提出了基于有界模型检验器CBMC的模型检验应用框架,包括航天测控数据的构造方法及验证性质的提取方法。随后,将该框架应用于外测数据处理软件,取得了良好的效果。

Research of Model Checking Application on Aerospace TT&C Software

Model checking is an efficient method to ensure software quality.However,complex input data and indistinct verification properties in large-scale aerospace TT&C software greatly hinders the application of model checking.After analyzing the characteristics of aerospace TT&C software and the difficulty of applying model checking,an application framework to aerospace TT&C software based on CBMC was proposed,including the construction method of aerospace measurement data and the extraction method of verification properties.The framework was then applied to the trajectory measurement data processing software and the result was satisfied.