The goal of this research is to develop a tool-based framework for the specification, analysis and implementation of real-time systems. The research includes three principal components: (1) a real-time specification language, (2) analysis techniques for showing that a specification is correct, and (3) a programming language in which the system is ultimately implemented. The specification component centers on the CSR paradigm, in which a real-time system's high-level control structure is entered as a set of Ada-like tasks, which are then compiled into a state-transition model. For the analysis component, an automated toolset based on the technique of finite-state abstraction is developed. The tools include a probabilistic reachability analyzer, a simulator and a model-checker. The language component is based on TCEL, a real-time programming language with CSR-style timing constructs. This feature allows the programmer to embed the real-time requirements within the program itself. A TCEL compiler is being developed, which rearranges the code to meet the inferred timing constraints.
