Automatically generating test cases for safety-critical software via symbolic execution

Automated test generation based on symbolic execution can be beneficial for systematically testing safety-critical software, to facilitate test engineers to pursue the strict testing requirements mandated by the certification standards, while controlling at the same time the costs of the testing process. At the same time, the development of safety-critical software is often constrained with programming languages or coding conventions that ban linguistic features which are believed to downgrade the safety of the programs, e.g., they do not allow dynamic memory allocation and variable-length arrays, limit the way in which loops are used, forbid recursion, and bound the complexity of control conditions. As a matter of facts, these linguistic features are also the main efficiency-blockers for the test generation approaches based on symbolic execution at the state of the art. This paper contributes new evidence of the effectiveness of generating test cases with symbolic execution for a significant class of industrial safety critical-systems. We specifically focus on SCADE, a largely adopted model-based development language for safety-critical embedded software, and we report on a case study in which we exploited symbolic execution to automatically generate test cases for a set of safety-critical programs developed in SCADE. To this end, we introduce an original test generator that we developed in a recent industrial project on testing safety-critical railway software written in SCADE, and we report on our experience of using this test generator for testing a set of SCADE programs that belong to the development of an on-board signaling unit for high-speed rail. The results provide empirically evidence that symbolic execution is indeed a viable approach for generating high-quality test suites for the safety-critical programs considered in our case study.