SPECIFICATION OF REALTIME SYSTEMS USING ASTRAL

ASTRAL is a formal specification language for realtime systems. It is intended to support formal software development and, therefore, has be en 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 specificat ions and a single global specification. This paper discusses the ratio nale of ASTRAL's design. ASTRAL's specification style is illustrated b y discussing a telephony example. Composability of one or more ASTRAL system specifications is also discussed by the introduction of a compo sition section, which provides the needed information to combine two o r more ASTRAL system specifications.