Real-time software that fails to meet a deadline can cause great damage, even loss of life. Static analysis is a safe way to verify real-time performance before the software is made operational, unlike testing which usually underestimates the worst-case execution time (WCET). Static analysis gives an upper bound on the WCET. Moreover, it can be done early in the software life-cycle, before the software is fully working, before the embedded hardware is available, and without any special simulations or other test environments. Thus, static analysis promises to be cheaper than testing and to find problems earlier, making them cheaper to correct.
Working at Space Systems Finland Ltd (SSF), a Finnish company specializing in custom software development for space projects, and with support from the European Space Agency, the author and his colleagues have developed a software tool called Bound-T which finds WCET bounds by static analysis of machine programs. At present the tool supports the Intel-8051, ADSP-21020 and SPARC V7 target architectures, with ARM7TDMI under implementation. The tool is being commercialized. This will require further research and development. The formation of a Finnish working group on static analysis is therefore very opportune.
We are interested in static analysis of executable (binary) programs, giving bounds on execution time and memory space and other properties that depend on the possible execution paths, the time/space/energy usage along the execution path, and the sequence of actions along the execution path. The goal is to verify the performance and to understand the performance factors.
Current work focuses on strengthening the analysis by means of constant propagation, program slicing, and optimized translation of the arithmetic instructions to Presburger arithmetic formulae for deriving loop repetition bounds. The assertion language, through which the user specifies execution scenarios and guides the analysis, is also being extended.
The analysis of feasible execution paths is our main future research problem. If all syntactic paths through the program's control-flow graphs and call graph are included in the computed WCET bound, the result is often much larger than the true WCET and may be uselessly large. To find the really feasible paths, the analysis must consider data state (variable values) as well as control state (program counter). The problem, of course, is the combinatorial explosion in the state space. There are many open questions: how should the set of feasible paths be formalized? Should the analysis use path enumeration, abstraction, or model checking? Can we use the same kind of path analysis for different purposes such as analysis of time, memory, pointers, or do specific purposes need specific analysis methods and path representations?