Successfully Coping with Scalability of Symbolic Analysis in Timing Analysis

ABSTRACT. Symbolic analysis is known and valued for its strength of statically inferring non-trivial properties of programs. This strength, however, comes typically at high computation costs often preventing a full path coverage of programs of real-world applications.

In this presentation we reconsider and highlight two examples of successfully coping and circumventing the scalabality issue related to straightforward applications of symbolic analysis in the timing analysis of real-time systems. In the first approach, we restrict symbolic analysis to program loops matching particular structural patterns for which symbolic analysis reduces to the solution of a set of recurrence equations which does not require an explicit symbolic path analysis and coverage of these loops. In the second approach, we focus the pathwise symbolic analysis of a program to a set of program paths which are known by other program analyses to be crucial for the timing behaviour of the program that is usually small and manageable. Both approaches have important complementary orthogonal applications in different stages of the timing analysis of safety-critical real-time systems and proved to be useful in practice.