Analyzing Partially-Implemented Real-Time Systems

We propose a method for analyzing partially-implemented real-time systems.Here we consider real-time concurrent systems for which some components areimplemented in Ada and some are partially specified using regular expressionsand Graphical Interval Logic (GIL), a real-time temporal logic. We show how toconstruct models of the partially-implemented systems that account for suchproperties as run-time overhead and scheduling of processes, yet supporttractable analysis of nontrivial programs. The approach can be fullyautomated, and we illustrate it by analyzing a small example.