Accelerating worst case execution time analysis of timed automata models with cyclic behaviour

摘要

The worst-case execution time (WCET) is an important property of safety-critical systems. In general, a safety-critical system can be analyzed using a formal model. An established formalism for modeling such systems is a timed automaton. Timed automata are finite automata, equipped with real-valued clocks. Transitions and locations can have constraints on these clocks, and clocks can be reset to zero. To make the analysis of timed automata feasible, the real-valued clocks must have a symbolic representation. This can be achieved using difference bounds matrices (DBMs), a data structure storing constraints on the difference values of two clocks.