模型检验在航天测控软件上的应用研究
|
摘要
模型检验是确保程序质量的有效手段,能弥补软件测试的不足。但航天测控软件规模大、输入数据复杂、验证性质不明确等因素极大地阻碍了模型检验的应用。针对航天测控软件,分析了其特点以及对其执行模型检验的困难,提出了基于有界模型检验器CBMC的模型检验应用框架,包括航天测控数据的构造方法及验证性质的提取方法。随后,将该框架应用于外测数据处理软件,取得了良好的效果。
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.
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.
引文
[1]王蓁蓁.模型检验综述[J].计算机科学,2013,40(Z6):1-14.
[2]CLARKE E M,EMERSON E A.Design and synthesis of synchronization skeletons using branching time temporal logic[C]∥Workshop on Logic of Programs.Springer,Berlin,Heidelberg,1981:52-71.
[3]CLARKE E M,EMERSON E A,SISTLA A P.Automatic verification of finite-state concurrent systems using temporal logic specifications[J].ACM Transactions on Programming Languages and Systems(TOPLAS),1986,8(2):244-263.
[4]CLARKE E,KROENING D,LERDA F.A tool for checking ANSI-C programs[C]∥International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Springer,Berlin,Heidelberg,2004:168-176.
[5]BALL T,RAJAMANI S.Checking temporal properties of software with boolean programs[C]∥Proceedings of the Workshop on Advances in Verification.2000:2-9.
[6]HOLZMANN G J.The SPIN Model Checker:Primer and Reference Manual[M].Addision-Wesley,2003.
[7]BEYER D,HENZINGER T A,JHALA R,et al.Checking memory safety with Blast[C]∥International Conference on Fundamental Approaches to Software Engineering.Springer,Berlin,Heidelberg,2005:2-18.
[8]GODEFROID P.Software model checking:The VeriSoft approach[J].Formal Methods in System Design,2005,26(2):77-101.
[9]Jpf project[OL].http://babelfish.arc.nasa.gov/trac/jpf.
[10]CIMATTI A,CLARKE EM,GIUNCHIGLIA F,et al.NuSMV:A new symbolic model checker[J].International Journal on Software Tools for Technology Transfer(STTT),2000,2(4):410-425.
[11]DELANGE J,PAUTET L,KORDON F.Design,implementation and verification of MILS systems[J].Software:Practice and Experience,2012,42(7):799-816.
[12]PERVEZ S,GOPALAKRISHNAN G,KIRBY R M,et al.Formal methods applied to high-performance computing software design:a case study of mpi one-sided communication-based locking[J].Software:Practice and Experience,2010,40(1):23-43.
[13]CHIAPPINI A,CIMATTI A,MACCHI L,et al.Formalization and validation of a subset of the European Train Control System[C]∥2010ACM/IEEE 32nd International Conference Software Engineering.IEEE,2010:109-118.
[14]BOCHOT T,VIRELIZIER P,WAESELYNCK H,et al.Model checking flight control systems:The airbus experience[C]∥Proceedings of the 31st International Conference on Software Engineering(ICSE 2009).Companion Volume,IEEE,2009:18-27.
[15]HAVELUND K,LOWRY M R,PENIX J.Formal analysis of a spacecraft controller using SPIN[J].IEEE Transactions on Software Engineering,2001,27(8):749-765.
[16]KROENING D,CLARKE E.The CPROVER User Manual[EB/OL].http://www.cprover.org/cbmc/doc/manual.pdf.
[17]METTA R.Verifying code and its optimizations:An experience report[C]∥2011IEEE Fourth International Conference Software Testing,Verification and Validation Workshops(ICSTW).IEEE,2011:578-583.
[18]CHEN T Y,CHEUNG S C,YIU S M.Metamorphic testing:a new approach for generating next test cases:Technical Report HKUST-CS98-01[R].Hong Kong:Department of Computer Science,Hong Kong University of Science and Technology,1998.
[19]董国伟,徐宝文,陈林,等.蜕变测试技术综述[J].计算机科学与探索,2009,32(2):130-143.
[2]CLARKE E M,EMERSON E A.Design and synthesis of synchronization skeletons using branching time temporal logic[C]∥Workshop on Logic of Programs.Springer,Berlin,Heidelberg,1981:52-71.
[3]CLARKE E M,EMERSON E A,SISTLA A P.Automatic verification of finite-state concurrent systems using temporal logic specifications[J].ACM Transactions on Programming Languages and Systems(TOPLAS),1986,8(2):244-263.
[4]CLARKE E,KROENING D,LERDA F.A tool for checking ANSI-C programs[C]∥International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Springer,Berlin,Heidelberg,2004:168-176.
[5]BALL T,RAJAMANI S.Checking temporal properties of software with boolean programs[C]∥Proceedings of the Workshop on Advances in Verification.2000:2-9.
[6]HOLZMANN G J.The SPIN Model Checker:Primer and Reference Manual[M].Addision-Wesley,2003.
[7]BEYER D,HENZINGER T A,JHALA R,et al.Checking memory safety with Blast[C]∥International Conference on Fundamental Approaches to Software Engineering.Springer,Berlin,Heidelberg,2005:2-18.
[8]GODEFROID P.Software model checking:The VeriSoft approach[J].Formal Methods in System Design,2005,26(2):77-101.
[9]Jpf project[OL].http://babelfish.arc.nasa.gov/trac/jpf.
[10]CIMATTI A,CLARKE EM,GIUNCHIGLIA F,et al.NuSMV:A new symbolic model checker[J].International Journal on Software Tools for Technology Transfer(STTT),2000,2(4):410-425.
[11]DELANGE J,PAUTET L,KORDON F.Design,implementation and verification of MILS systems[J].Software:Practice and Experience,2012,42(7):799-816.
[12]PERVEZ S,GOPALAKRISHNAN G,KIRBY R M,et al.Formal methods applied to high-performance computing software design:a case study of mpi one-sided communication-based locking[J].Software:Practice and Experience,2010,40(1):23-43.
[13]CHIAPPINI A,CIMATTI A,MACCHI L,et al.Formalization and validation of a subset of the European Train Control System[C]∥2010ACM/IEEE 32nd International Conference Software Engineering.IEEE,2010:109-118.
[14]BOCHOT T,VIRELIZIER P,WAESELYNCK H,et al.Model checking flight control systems:The airbus experience[C]∥Proceedings of the 31st International Conference on Software Engineering(ICSE 2009).Companion Volume,IEEE,2009:18-27.
[15]HAVELUND K,LOWRY M R,PENIX J.Formal analysis of a spacecraft controller using SPIN[J].IEEE Transactions on Software Engineering,2001,27(8):749-765.
[16]KROENING D,CLARKE E.The CPROVER User Manual[EB/OL].http://www.cprover.org/cbmc/doc/manual.pdf.
[17]METTA R.Verifying code and its optimizations:An experience report[C]∥2011IEEE Fourth International Conference Software Testing,Verification and Validation Workshops(ICSTW).IEEE,2011:578-583.
[18]CHEN T Y,CHEUNG S C,YIU S M.Metamorphic testing:a new approach for generating next test cases:Technical Report HKUST-CS98-01[R].Hong Kong:Department of Computer Science,Hong Kong University of Science and Technology,1998.
[19]董国伟,徐宝文,陈林,等.蜕变测试技术综述[J].计算机科学与探索,2009,32(2):130-143.