The reliability of software is an increasingly important demand,
especially for safety critical systems. RAISE is a mathematically
based method which has been shown to be useful in the industrial
development of many kinds of software systems. However, RAISE has no
particular features for specifying real-time requirements, which often
occur in safety critical systems. Adding time constructors, like wait,
to RAISE will make the new specification language, Timed RAISE
Specification Language (TRSL), and give it the power of specifying
real-time application. Then the work of finding theoretical foundation
for TRSL comes. In this report, the Operational Semantics of TRSL will
be first introduced.  Then we will define a pre-order and test
equivalence relation for TRSL.  Proof rules for TRSL are listed in the
Appendix B. Their soundness corresponding to our operational model are
also explained.