A Symbolic Execution Optimization Method for Safety-critical Software System

doi:10.3969/j.issn.1006-2475.2020.01.018

Abstract

Abstract: In the aviation, nuclear power and defense military fields, the software of the Safety-Critical System (SCS) is very important, and its reliability must be guaranteed by testing or formal methods. Symbolic execution is widely used as an efficient test case generation method. However, the coupling between the modules of SCS software system is high, which makes symbolic execution constraint solving difficult. This paper proposes a decoupling method with a minimum set of weights to provide a new idea for the automated testing of safety-critical software systems.

Key words: safety-critical system, software coupling, weighted minimum cut set, symbolic execution

CLC Number:

TP311

DAI Yan-jun1, WU Zhi-qiang2, LIU Jie1, LIU Zhao-hui1, CHEN Zhi2, XIAO An-hong2. A Symbolic Execution Optimization Method for Safety-critical Software System[J]. Computer and Modernization, doi: 10.3969/j.issn.1006-2475.2020.01.018.

References

［1］ LEVESON N G. Software safety: Why, what, and how［J］. ACM Computing Surveys, 1986,18(2):125-163.
［2］ NAYLOR A W, VOLZ R A. Design of integrated manufacturing system control software［J］. IEEE Transactions on Systems， Man， and Cybernetics, 1987,17(6):881-897.
［3］ KUSHAL K S, NANDA M, JAYANTHI J. Formal methods and tools for safety of critical systems［M］// Formal Methods for Safety and Security. 2018:13-21.
［4］ KING J C. Symbolic execution and program testing［J］. Communications of the ACM, 1976,19(7):385-394.
［5］ SEN K. Concolic testing［C］// Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering. 2007:571-572.
［6］ CHIPOUNOV V, GEORGESCU V, ZAMFIR C, et al. Selective symbolic execution［C］// Proceedings of the 5th Workshop on Hot Topics in System Dependability. 2009:1286-1299.
［7］ CADAR C, SEN K. Symbolic execution for software testing: Three decades later［J］. Communications of the ACM, 2013,56(2):82-90.
［8］秦晓军,周林,陈左宁,等. 基于懒符号执行的软件脆弱性路径求解算法［J］. 计算机学报, 2015(11):2290-2300.
［9］黄晖,陆余良,刘林涛,等. 控制流污点信息导向的符号执行技术研究［J］. 中国科学技术大学学报, 2016(1):21-27.
［10］罗荣森. 基于符号摘要的动态符号执行的研究［D］. 成都：电子科技大学, 2016.
［11］CADAR C, SEN K. Symbolic execution［C］// International Conference on Runtime Verification. Springer, Berlin, Heidelberg, 2012:2.
［12］张羽丰. 符号执行可扩展性及可行性关键技术研究［D］. 长沙：国防科学技术大学， 2013.
［13］李航, 臧洌,甘露. 基于蚁群算法的猜测符号执行的路径搜索［J］. 计算机科学, 2018,45(6):151-156.
［14］LI X, LIANG Y, QIAN H, et al. Symbolic execution of complex program driven by machine learning based constraint solving［C］// IEEE/ACM International Conference on Automated Software Engineering. 2016:554-559.
［15］RAKADJIEV E, SHIMOSAWA T, MINE H, et al. Parallel SMT solving and concurrent symbolic execution［C］// Proceedings of 2015 IEEE Trustcom/BigDataSE/ISPA. 2015,3:17-26.
［16］CADAR C, DUNBAR D, ENGLER D. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs［C］// Proceedings of the USENIX Symposium on Operating Systems Design and Implementation. 2008:209-224.
［17］SHINNERS S M, ADELMAN S. Modern control system theory and application［J］. IEEE Transactions on Systems, Man, and Cybernetics, 1997,9(6):365-366.
［18］刘志凯,王嵚峰,王冬,等. 基于FPGA的算法组态技术在安全级数字化I&C中的应用［J］. 仪器仪表用户, 2017,24(11):53-56.
［19］COLACO J L, PAGANO B, POUZET M. SCADE 6: A formal language for embedded critical software development［C］// International Symposium on Theoretical Aspects of Software Engineering. 2017:1-11.
［20］CADAR C, GANESH V, PAWLOWSKI P M, et al. EXE:Automatically generating inputs of death［C］// Proceedings of the 13th ACM Conference on Computer and Communications Security. 2006:322-335.
［21］STOER M, WAGNER F. A simple min-cut algorithm［J］. Journal of the ACM, 1997,44(4):585-591.
［22］GEISSMANN B, GIANINAZZI L. Parallel minimum cuts in near-linear work and low depth［C］// The 30th Symposium on Parallelism in Algorithms and Architectures. 2018.
［23］MOURA L D, BJRNER N. Z3: An efficient SMT solver［C］// Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Held as Part of the Joint European Conferences on Theory and Practice of Software. 2008:337-340.
［24］DETERS M, REYNOLDS A, KING T, et al. A tour of CVC4: How it works, and how to use it［C］// Proceedings of the 14th Conference on Formal Methods in Computer-aided Design. 2014:7.

[1]	LI Tong, DING Guo-fu. A Symbolic Execution Technology Supporting Multi-thread Program [J]. Computer and Modernization, 2020, 0(06): 60-.
[2]	FAN Yu. Research on Path Feasibility Detection Based on Symbolic Execution and Data Mining [J]. Computer and Modernization, 2013, 1(3): 74-77.