Abstract
A Theorem Prover for ASTRAL
by: Paul Z. Kolano
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.
Keywords:
real-time systems, automated deduction, PVS, theorem proving,formal methods, formal specification and verification, ASTRAL
Date:
January 1998
Document: 1998-01
