Automatic generation of high quality test sets via CBMC

摘要: Software Testing is the most used technique for software verication in industry. In case of safety critical software, test set can be required to cover a high percentage (up 100%) code according some metrics. Unfortunately, attaining such percentages not easy using standard automatic tools tests generation, and manual generation by domain experts often necessary, thereby signicantly increasing associated costs. previous papers, we have shown how it possible automatize process C programs via bounded model checker CBMC. particular, productively use CBMC sets covering 100% branches 5 modules ERTMS/ETCS, industrial Ansaldo STS. automatically generated, lower \quality" if compared manually generated experts: Both attained desired branch coverage, but sizes are roughly twice corresponding ones. Indeed, contain redundant tests, i.e. that do contribute reach coverage. These useless from perspective detect then eliminate posteriori, and, maintained, imply additional costs during process. this paper present new methodology \high quality" guaranteeing full Given an initially empty T , basic idea extend with as many which covered . This requires analysis control ow graph