This award addresses the need for improving system reliability through better software development methods and tools, and specifically, through applying formal methods to the development of realtime systems. The solution sought is a formal framework for the specification and analysis of realtime systems. This framework is based on the ASTRAL formal specification language and includes the ASTRAL language for writing requirements and design specifications of realtime systems, a formal proof theory for proving properties about ASTRAL specifications, and a support environment for the construction and analysis of the specifications. The tools that make up the support environment are a syntax-directed editor, an ASTRAL to TRIO translator, an ASTRAL specification processor, and a mechanical theorem prover. The TRIO-based model checkers, developed at the Politecnico di Milano, are being integrated into the support environment. The main theoretical issues to be investigated deal with the composability of ASTRAL specifications. The research is developing a proof theory that prescribes how the proofs of the individual state machine specifications can be combined to produce a proof of the entire system. Another composability issue to be investigated is the composition of two or more ASTRAL system specifications (i.e., a global specification and its associated collection of state machine specifications) to derive the specification for the composite system. ASTRAL is being used to specify complex realtime systems taken from a variety of application areas to evaluate its effectiveness and utility.
