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

摘要/Abstract

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

关键词: CBMC, 航天测控软件, 模型检验, 蜕变测试

Abstract: 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.

Key words: Aerospace TT&C software, CBMC, Metamorphic testing, Model checking

中图分类号:

TP311

李运筹,尹平. 模型检验在航天测控软件上的应用研究[J]. 计算机科学, 2018, 45(6A): 523-526. https://doi.org/

LI Yun-chou,YIN Ping. Research of Model Checking Application on Aerospace TT&C Software[J]. Computer Science, 2018, 45(6A): 523-526. https://doi.org/

参考文献

[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 Refe- rence Manual[M].Addision-Wesley,2003.
[7]BEYER D,HENZINGER T A,JHALA R,et al.Checking memo- ry 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 ap- proach[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,implementa- tion 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]∥2010 ACM/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]∥2011 IEEE 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.

相关文章 15

[1]	阳小华, 闫仕宇, 刘杰, 李萌. 科学计算程序蜕变关系层次分类模型 Hierarchical Classification Model for Metamorphic Relations of Scientific Computing Programs 计算机科学, 2020, 47(11A): 557-561. https://doi.org/10.11896/jsjkx.200200015
[2]	王颖洁, 周宽久, 李明楚. 实时嵌入式系统的WCET分析与预测研究综述 Survey of WCET Analysis and Prediction for Real-time Embedded Systems 计算机科学, 2019, 46(6A): 16-22.
[3]	张兴隆,于磊,侯雪梅,侯韶凡. 面向对象程序蜕变关系构造方法 Method of Metamorphic Relations Constructing for Object-oriented Software Testing 计算机科学, 2017, 44(Z11): 485-489. https://doi.org/10.11896/j.issn.1002-137X.2017.11A.103
[4]	刘斌斌,刘万伟,毛晓光,董威. 无人驾驶汽车决策系统的规则正确性验证 Correctness Verification of Rules for Unmanned Vehicles’ Decision System 计算机科学, 2017, 44(4): 72-74. https://doi.org/10.11896/j.issn.1002-137X.2017.04.015
[5]	陈光颖,黄志球,陈哲,阚双龙. 面向DO-333的襟缝翼控制单元安全性分析 Safety Analysis of Slat and Flap Control Unit for DO-333 计算机科学, 2016, 43(5): 150-156. https://doi.org/10.11896/j.issn.1002-137X.2016.05.028
[6]	惠战伟,黄松,张婷婷,刘剑豪. 一种基于蜕变关系的测试与失效测试用例定位模型 Testing and Invalid Testing Case Localization Model Based on Metamorphic Relation 计算机科学, 2016, 43(10): 57-62. https://doi.org/10.11896/j.issn.1002-137X.2016.10.010
[7]	朱利鲁,李智. 问题框架中问题领域因果行为的形式化验证 Formal Validation of Causal Behaviors of Problem Domains in Problem Frames Approach 计算机科学, 2015, 42(12): 136-142.
[8]	开金宇,缪淮扣,高洪皓. Web服务计算组合流程QoS验证 Verification QoS of Web Services Compositional Processes 计算机科学, 2015, 42(12): 120-123.
[9]	王飞,沈国华,黄志球,马琳,刘畅,李海峰,廖莉莉. 一种结合线性时序逻辑和故障树的软件安全验证方法 Method Combining Linear Temporal Logic and Fault Tree for Software Safety Verification 计算机科学, 2015, 42(12): 71-75.
[10]	王蓁蓁. 模型检验综述 Survey of Model Checking 计算机科学, 2013, 40(Z6): 1-14.
[11]	张媛，于冠龙，李仁见. 一种基于模型检验的缓冲区溢出检测方法 Buffer Overflow Detection Method Based on Model Checking 计算机科学, 2012, 39(Z6): 31-34.
[12]	罗莉，欧国东，刘彬，徐炜遐，窦强. 异步FIFO的模型检验方法 Symbolic Model Checking of Asynchronous FIFO 计算机科学, 2012, 39(3): 268-270.
[13]	王榕贲可荣. 蜕变关系构造基本准则与策略研究 Researches on Basic Criterion and Strategy of Constructing Metamorphic Relations 计算机科学, 2012, 39(1): 115-119.
[14]	王志坚，李雯睿,杨种学,张鹏程. 基于uMSD的Web服务组合验证方法研究 Research on Verification of Web Service Composition Based on uMSD 计算机科学, 2011, 38(9): 119-125.
[15]	叶俊民，谢茜，金聪，李明，张振方. 一种基于模型检验程序分析技术的前端工具研究 Research on a Front-end Tool for Program Analysis Based on Model Checking 计算机科学, 2010, 37(5): 118-122174.

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed