A Formal Framework for ASTRAL Inter-Level Proof Obligations

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 how to formally prove the mathematicalcorrectness of ASTRAL specifications. ASTRAL is provided with structuringmechanisms that allow one to build modularized specifications of complexsystems with layering. A realtime system is modeled by a collection of processspecifications and a single global specification. Each process specificationconsists of a sequence of levels; each level is an abstract data type view ofthe process being specified. In this paper further details of the ASTRALrefinement process, which were not fully developed in previous papers, arepresented. Formal proofs in ASTRAL can be divided into two categories:inter-level proofs and intra-level proofs. The former deal with proving thatthe specification of level i+1 is consistent with the specification of level i,while the latter deal with proving that the specification of level i isconsistent and satisfies the stated critical requirements. This paperconcentrates on inter-level proofs. The necessary proof obligations to assurethat a refinement is a correct implementation are presented. The approach ismotivated with a communication example.