Duncan Clarke, Thierry Jéron, Vlad Rusu, Elena Zinovieva. STG: A Symbolic Test Generation Tool. In Joost-Pieter Katoen, Perdita Stevens, editors, Tools and Algorithms for the Construction and Analysis of Systems, 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings. Volume 2280 of Lecture Notes in Computer Science, pages 470-475, Springer, 2002. [doi]
Applying formal methods to testing has recently become a quite popular research topic. In this paper we explore the opposite approach, namely, applying testing techniques to formal verification. The idea is to use test generation techniques to extract subsets (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.