Counter Automata for Parameterised Timing Analysis of Box-Based Systems

We present a new compositional approach for analysing the resource usage of reactive box-based systems, as exemplified by Hume. Our analysis deals with a key aspect of reactivity, namely determining the worst-case execution time between some external input event and the associated output event, taking into account repeated box iterations and the possible interactions between boxes in terms of input/output values. In order to achieve this, we capture the system behaviour by abstract interpretation, obtaining counter automata, finite state automata with additional counters that can be used to represent sizes/resource costs and control repetitions. These counter automata precisely capture cost information from the original box-based system, but in a way that is more abstract and therefore easier to analyse. The key contribution of this paper over previous work is that we are able to analyse box-based computations for cyclic systems whose costs may depend on some input parameters and in which the cost formulae are non-linear.