How to test a program with no available source code is of great importance for software quality assurance in practice, but still remains a challenge. In this paper, we describe a novel approach to tackling this challenge. Its principal idea is first to formalize the informal requirements into formal operation specifications based upon program interface scenarios, and then utilize the specifications as a foundation for test case generation and test result analysis. We discuss how the formal specifications can be achieved and how formalization benefits the testing. In particular, we focus on the issue of how to test whether all functional scenarios defined in a specification are correctly implemented in the program. We present an example of applying the approach to an IC Card system to demonstrate its usage and to analyze its potential capability and challenges in practice.