This paper discusses the adaptation of the PVS theorem prover for performing analysis of real-time systems written in the ASTRAL formal specification language. A number of issues were encountered during the encoding of ASTRAL that are relevant to the encoding of many real-time specification languages. These issues are presented as well as how they were handled in the ASTRAL encoding. A translator has been written that translates any ASTRAL specification into its corresponding PVS encoding. After performing the proofs of several systems using the encoding, PVS strategies have been developed to automate the proofs of certain types of properties. In addition, the encoding has been used as the basis for a transition sequence generator tool.