Report ID
1998-01
Report Authors
Paul Z. Kolano
Report Date
Abstract
The ASTRAL real-time formal specification language has been encoded into thePVS theorem prover. A translator has been developed to completely translateany single-level ASTRAL specification into its corresponding PVS encoding. Thesemantics of the ASTRAL abstract machine have been revised and expanded for usewith PVS. This paper describes the encoding and semantics and explains theiruse along with providing additional applications of the encoding.
Document
1998-01.ps444.28 KB