V-V method that overcome Black-Box tesing problem:
1. Model checking can produce minimal sets of test cases that guarantee certain coverage criteria for example by using symbolic execution modes of the model checker (mitigates conditions a and f).
2. Dedicated test systems providing test harness infrastructure can be used to automate test execution (for example, for regression tests, mitigating e).
3. Dedicated verification runtime environments (e.g., virtual machines) can be used to simulate the program environment that cannot be controlled from a test application. These runtimes can also perform complex non-functional checks and defect analysis (mitigating b and c).
4. Code annotations can be used in combination with specific virtual machines (VMs) or code generators to automatically create and run test cases (which saves the effort of manually creating test harnesses and/or explicit code instrumentation). This is especially helpful for achieving the “test-like-you-fly/fly-like-you-test” goal. Verification-oriented runtime systems (like a program model checker) also enable checking non-functional properties that would otherwise not be amenable to testing (e.g., “no memory allocation in function x” or “function y has to be reentrant”). This mitigates c, d, and e.
5. Contracts in the code can be used to specify fine-grained properties, which reduces the black box property to check to a generic “don’t violate any contracts” (this is especially helpful to avoid “accidental correctness”).