Early Results from Characterizing Verification Tools through Coding Error Candidates Reported in Space Flight Software

Abstract

Six software verification tools have been applied to space flight software and the findings reported by each tool have been compared in order to derive footprints of the tools regarding capabilities of fault identification. Currently available results are provided in this paper: sensitivity and precision of individual tools and combinations of pairs of tools out of the set. A reader should bear in mind that the results as presented here depend on the spectrum of fault types as present in the reference software and on the configuration of tools towards real defects and fault types which are of interest for embedded systems and space flight software.