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

https://doi.org/10.1016/j.entcs.2016.01.004Get rights and content
Under a Creative Commons license
open access

Abstract

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.

Keywords

Test generation
cyclic executive
C Code
automotive controllers
experimentation
CBMC
Frama-C

Cited by (0)

1

This work is supported by NECSIS (Network for the Engineering of Complex Software-Intensive Systems for Automotive Systems) of NSERC, Canada. We would like to acknowledge Alexandre Petrenko, lead researcher of MODL team at CRIM, for his comments and revision on early versions of this paper.