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.

There are several tools for the analysis of timed automata, with the tool Uppaal being probably the most prominent. Typical properties that can be checked by this tool are safety and liveness properties; however, Uppaal can also be used to establish the worst-case execution time.

This paper concentrates on the latter and presents an approach to efficiently compute the WCET for a timed automaton. Although the topic is quite specific, the paper is accessible for a general audience. It begins by introducing timed automata, difference bounds matrices (DBMs), and the corresponding algorithms. The contribution of the paper is the modification of the standard algorithms to compute the WCET. The main idea is to introduce a new clock to keep track of the execution time. Then, the algorithms are adapted to handle the normal clocks and the newly introduced clock differently. Because loops can increase the state space significantly, abstractions for handling loops are presented that are specific to the WCET computation. Throughout the paper, there are examples of timed automata that illustrate both general ideas and special cases. Finally, the paper shows that a prototype implementation of the presented algorithm outperforms Uppaal in the WCET computation significantly.