Formally specifying and verifying real-time systems

A real time computer system is a system that must perform its functions within specified time bounds. These systems are generally characterized by complex interactions with the environment 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. One way to achieve this reliability is through formal development. Although research in the area of real time systems has been quite active and a number of experimental environments supporting formal specifications have been developed, the search for adequate notations and tools is still ongoing. In order to get designers to use formal methods to develop real time systems it is necessary to provide them with an integrated set of tools for writing and analyzing their specifications. The ASTRAL Software Development Environment (SDE), which is an integrated set of tools based on the ASTRAL formal framework, is intended to meet this need. The tools that make up the support environment are a syntax directed editor, a specification processor, a verification condition generator, a mechanical theorem prover, and a browser kit. The paper discusses the goals for ASTRAL, why they were important, and how they were met. It also gives an overview of the ASTRAL Software Development Environment.