An Integer Static Analysis for Better Extrapolation in Uppaal

Extended Timed Automata (XTA) is a widely used formalism to show the correctness of industrial applications. The decidability results and current extrapolations for XTA are based on constants in the automaton. However, in the case of XTA such bounds depend on integer variables or variable expressions. Since computing such bounds can be as expensive as the verification task, tools such as Uppaal over-approximate the bounds by values given in the type definitions. These values are excessively large and can yield huge state spaces. In this paper we outline a targeted static analysis to efficiently over-approximate location based invariants (and thereby ranges) of integer variables. We have implemented our analysis in Uppaal where the new tighter bounds are available to all currently implemented extrapolation operations. Our experiments show an exponential reduction in the state space of several models. In addition, the computation overhead introduced by the integer static analysis is negligible.