Evaluation of Verification Tools Continued: More Tools, More Software, More Aspects

In a previous study six software verification tools have been applied to a representative space software package. The findings reported by each tool have been compared in order to derive footprints regarding fault identification. In a continuation three more tools were applied to the previously selected application software and to another application together with two tools previously used in order to broaden the base of evaluation. More aspects were considered regarding the evaluation of results: an additional evaluation criterion was added and a comparison of reported defects with the outcome of unit tests was performed. Due to a higher degree of formalization and automation the manual evaluation effort could be decreased while extending the number of considered reports and the number of tools. The encountered evaluation and verification issues are discussed in detail. All results together shall provide a detailed view on the defect identification capabilities of the considered tools w.r.t. current software base. Altogether, the high quality of reports as obtained in the previous study was not obtained again: in context of a different set of tools and another (object-oriented) language a lot of trivial reports were observed.