Improving the automatic test generation proces for Coverage Analysis using CBMC

Software Testing via Coverage Analysis is the most used technique for software verification in industry, but, since manual generation is involved, remains one of the most expensive process of the software development. Many tools have been proposed for the automatic test generation: on one hand they reduce the cost of the testing generation process, on the other hand the quality of the test set so generated is lower than the quality of the test set manually generated by domain experts. In fact, most of the time, the test set automatically generated contains redundant tests, i.e. test that does not contribute to reach the property of 100% of coverage: if they are eliminated by the set, the property still holds. Indeed, these redundant tests are useless from the perspective of the coverage, are not easy to detect and then to eliminate a posteriori, and, if maintained, imply additional costs during the verification process. In this paper we present a methodology for the automatic generation of test set for Coverage Analysis, containing only non redundant test. We experimented it on a subset of modules of the ERTMS/ETCS source code, an industrial system for the control of the traffic railway, provided by Ansaldo STS, where we were able to verify completely 31 different modules of the ERTMS: On 20 modules we were able to generate a set of minimal test covering the 100% of the code for each function in each module; on 7 of them we generate a set of tests that does not cover the 100% of the branches due to unreachable code; the last 4 modules were not completely verified due to CBMC exponential blow-up explosion. The use of our methodology for test generation led to a dramatic increase in the productivity of the entire Software Development process by substantially reducing the number of tests generated and thus the costs of the testing phase.