Proof assistance for real-time systems using an interactive theorem prover

This paper discusses the adaptation of the PVS theorem prover for performing analysis of real-time systems written in the ASTRAL formal specification language. Several issues arose during the encoding of ASTRAL that are relevant to the encoding of many real-time specification languages such as encoding formulas as types, handling partial functions, dealing with noninterleaved concurrency, and defining irregular operators. These issues and...