Verification Using Test Generation Techniques

摘要

Applying formal methods to testing has recently become a popular research topic. In this paper we explore the opposite approach, namely, applying testing techniques to formal verification. The idea is to use symbolic test generation to extract subgraphs (called components) from a specification and to perform the verification on the components rather than on the whole system. This may considerably reduce the verification effort and, under reasonable sufficient conditions, a safety property verified on a component also holds on the whole specification. We demonstrate the approach by verifying an electronic purse system using our symbolic test generation tool STG and the PVS theorem prover.