The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.08 - August (1994 vol.20)
pp: 548-561
ABSTRACT
<p>ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL specifications. ASTRAL is provided with structuring mechanisms that allow one to build modularized specifications of complex systems with layering. In this paper, further details of the ASTRAL environment components and the critical requirements components, which were not fully developed in previous papers, are presented. Formal proofs in ASTRAL can be divided into two categories: interlevel proofs and intralevel proofs. The former deal with proving that the specification of level i+1 is consistent with the specification of level i, and the latter deal with proving that the specification of level i is consistent and satisfies the stated critical requirements. This paper concentrates on intralevel proofs.</p>
INDEX TERMS
formal specification; real-time systems; finite state machines; program verification; specification languages; intralevel proof obligations; ASTRAL; formal specification language; real-time systems; formal software development; mathematical correctness; formal methods; formal specification; verification; timing requirements; formal proof; state machines; ASLAN; TRIO
CITATION
R.A. Kemmerer, D. Mandrioli, "A Formal Framework for ASTRAL Intralevel Proof Obligations", IEEE Transactions on Software Engineering, vol.20, no. 8, pp. 548-561, August 1994, doi:10.1109/32.310665
22 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool