Towards Compositional Worst-Case Execution Time Analysis for Hume Programs

In order to safely construct time-critical systems, it is necessary to ensure that responses are produced in accordance with the required time deadlines. This requires us to determine safe upper bounds on the worst-case execution time (WCET) for each primitive action, and then to combine these WCETs to determine overall WCETs for each response.Our overall objective is to perform WCET analysis for reactive, hard real-time programs written in the very high-level language Hume, which combines purely functional expressions into a network of reactive, asynchronous “boxes”. The WCET analysis for each box is per- formed using an automatic amortised cost analysis, based on the Hume operational semantics. This analysis generates a set of constraints that can be solved using standard linear program- ming techniques. This paper considers how to construct a WCET analysis for a network of compositions of Hume boxes from the WCETs for each individual box. The main novel contri- bution of this paper is the treatment of abstract program values. In particular, we deal with the constraints that are induced by dynamic changes to program values, and with repetitive execution of box compositions. In order to increase the precision of our analysis, we distinguish between several different situations in which boxes may be used. Each situation is expressed in terms of abstract input values and assigned an independent WCET. In contrast to most other work on WCET analysis, the solutions that we obtain from our analysis provide a function for the WCET in terms of abstract program values