Test Data Generation for Cyclic Executives with CBMC and Frama-C: A Case Study

Testers of cyclic executive systems are required to make considerable and repetitive efforts to determine input sequences (tests) for leading a system from a start state to a target state. This task is time-consuming and it might lead testers to produce fewer tests than required; which affects negatively the quality of systems and can reduce time-to-market. We propose an automated test generation approach which integrates two renowned tools: the code slicing plugin of Frama-C and the bounded model-checker CBMC. We also suggest several code metrics to better assess the complexity of code and the effect of code slicing on test derivation with CBMC. The proposed approach has been tested on industrial case studies and significantly reduces test generation effort and computation time on two automotive controllers. The proposed approach alleviates the workload of testers so they are able to focus on producing more tests; thus, increasing the quality of systems.