Specification of Realtime Systems Using ASTRAL

ASTRAL is a formal specification language for realtime systems. It is intendedto support formal software development and, therefore, has been formallydefined. The structuring mechanisms in ASTRAL allow one to build modularizedspecifications of complex systems with layering. A realtime system is modeledby a collection of state machine specifications and a single globalspecification. 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 bythe introduction of a composition section, which provides the neededinformation to combine two or more ASTRAL system specifications into a singlenew one. Finally, this paper discusses the current status of the ASTRALsoftware development environment.