Unifying Verification and Validation Techniques: Relating Behavior and Properties through Partial Evidence

摘要

The past decade has produced a range of techniques for assessing the correctness of software systems. These techniques, such as various forms of static analysis, automated verification, and test generation, are capable of producing a variety of forms of evidence showing that the software behavior meets its specified properties. We contend that, as currently formulated, existing techniques fail to externalize all of the useful pieces of evidence that they compute which limits the opportunities to obtain a comprehensive and accurate assessment of property-behavior conformance. Explicitly accounting for the ways that V&V techniques produce partial evidence offers the potential to look beyond the boundaries of individual analysis, verification, and testing techniques to consider the larger question of how the techniques fit together to provide an explicit body of evidence about software system quality.