Issue No. 09 - September (1997 vol. 23)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.629494
<p><b>Abstract</b>—ASTRAL is a formal specification language for realtime systems. It is intended to support formal software development and, therefore, has been formally defined. The structuring mechanisms in ASTRAL allow one to build modularized specifications of complex systems with layering. A realtime system is modeled by a collection of state machine specifications and a single global specification. This paper discusses the rationale of ASTRAL's design. ASTRAL's specification style is illustrated by discussing a telephony example. Composability of one or more ASTRAL system specifications is also discussed by the introduction of a composition section, which provides the needed information to combine two or more ASTRAL system specifications.</p>
Formal methods, formal specification and verification, assertions, temporal logic, realtime systems, timing requirements, state machines, composability, ASLAN, TRIO.
R. A. Kemmerer, C. Ghezzi and A. Coen-Porisini, "Specification of Realtime Systems Using ASTRAL," in IEEE Transactions on Software Engineering, vol. 23, no. , pp. 572-598, 1997.