Formal Verification of Realtime Systems in ASTRAL

ASTRAL is a formal specification language for realtime systems. It is intendedto support formal software development, and therefore has been formallydefined. This paper focuses on formally proving the mathematical correctnessof ASTRAL specifications. ASTRAL is provided with structuring mechanisms thatallow one to build modularized specifications of complex systems withlayering. In this paper, we exploit and enhance ASTRAL\'s structure and providea proof method that allows one to build well structured proofs. Correctnessproofs in ASTRAL can be divided into two categories: inter- level proofs andintra-level proofs. The former deal with proving that the specification oflevel i+1 is consistent with the specification of level i, while the latterdeal with proving that the specification of level i is correct. In this paperwe concentrate on intra-level proofs. 1992-25