The goals of the proposed project are to investigate techniques that support timing and race condition verification for real-time systems. We aim at high confidence embedded systems and plan to implement a tool suite to automate a test and verification process, as well as static and runtime analysis approaches. The objectives of the project are to design a temporal analysis mechanism that has the following attributes:

• Through instrumentation and dynamic analysis of program execution, the temporal dependence between program behavior and the timing of event occurrences can be exposed, modeled, and evaluated.
• To constitute an automated testing framework for effective application of timed test stimuli.
• By adopting temporal interval logic, formal reprensentation of system behavior at implementation level of abstraction can be realized for verification of timing properties.

Particularly, the project is aimed to explore any potential execution derivations or race conditions when sequences of test events occur at various instances. Combined with execution trace and temporal interval logic analysis, alternate timing patterns can be generated to improve test coverage. In addition, comparisons of formal representations at implementation and at specification levels can be carried out for timing verification.

While we devise new efficient algorithms or adapt existing ones (that are complementary to the study we propose) for timing analysis, our main focus will be on integration and experiment for practical real-time systems. Experiment and validation in NASA's applications will be conducted such that we can identify practical implementation constraints, improve the flexibility of the proposed methodology, and measure the effectiveness of the research approaches. In addition, collaborations with other IV&V teams will be initiated for technology demonstration, discussion, and dissemination.