The RAISE Specification Language has no ``real time'' features. So, it is difficult to use it to specify real time applications. Now, we consider adding time to RSL. Our first attempt following Anne Haxthausen's proposal of encoding DC in RSL, we set up a proof assistant called DC/RJ. It is constructed from encoding of both DC semantics and proof system of Interval Logic and DC, and uses the RAISE Justification tool to do the verification for DC. In this paper, the author first introduces how DC can be integrated with RSL in detail. Then the construction and hierarchy of DC/RJ are explained. The Gas Burner example is used to show how DC/RJ works. A comparison among DC proof assistant systems, the problems and perspectives of our system are discussed at the end.
