As computers become ubiquitous, they are increasingly used in safety critical environments. Typical safety applications are control systems, monitoring systems and communication systems. Any failure of such computer systems may cause a great financial loss, environmental disaster or even the loss of lives. The potential high cost associated with an incorrect operation of these systems has created a demand for a rigorous framework in which various design alternatives can be formally specified and rigorously analyzed and tested before implementation. It is commonly believed that future safety critical systems uill be more complex due to increased demands on their functionalities, as well as, the size of the problem domain. Thus, it will be difficult to analyze and test the correctness without computer-aided tools. One common aspect of all safety critical systems is that they must respond under stringent realtime constraints. That is, their correctness depends not only on how concurrent components interact, but also on the time at which these interactions occur. These systems are costly to prototype, requiring careful prediction of timing properties before implementation and evaluation of design alternatives. Thus, it is important to develop a formal framework that supports automatic and computer-aided analysis and testing to effectively cope with increased complexity. The major thrust of this research is to develop analysis and testing techniques for timing properties, and to implement supporting software tools based on real-time temporal logic and state machine models. The proposed tools will provide an environment in which software engineers can generate tests from behavioral specifications and performance requirement constraints and simulate and test to validate the specification.
