The time dependent and asynchronous nature of many real-time applications adds a new and potentially difficult element to the testing activities, which needs to be solved. To address this need, we present a formal testing strategy for real-time software by using dual-language approach. In our approach, we start out with the derivation of real-time software requirements in temporal logic form as our basis of descriptive formalism. Then we presented an abstract semantics to correlate the temporal logic formulae with the time Petri nets of the software, which is the operational formalism, and is used to generate the test cases. Based on the temporal properties of the software requirements, the descriptive formalism provides rich information for test oracle generation. By combining the timed test cases with oracles, the firm and definite test suites are formed.