ASTRAL: an Assertion Language for Specifying Realtime Systems

: ASTRAL is a formal specification language for realtime systems. This paper discusses the rationale of ASTRAL's design and shows how the language builds on previous language experiments. ASTRAL is intended to support formal software development; therefore, the language itself has been formally defined. ASTRAL's specification style is illustrated by discussing a case study taken from telephony. 1. Introduction Realtime computer systems are increasingly being used in critical applications such as aircraft avionics, nuclear power plant control and patient monitoring. These systems are generally characterized by complex interactions with the environments in which they operate, and strict time constraints whose violation may have catastrophic consequences. The need for these software systems to be highly reliable is evident. The best way to improve software quality is to develop it formally. Existing informal software development methods and tools [HP 88, Qui 85, Gom 86] are simply unab..