Finding best and worst case execution times of systems using difference-bound matrices

Abstract

The paper provides a solution to the fundamental problems of computing the shortest and the longest time taken by a run of a timed automaton from an initial state to a final state. It does so using the difference-bound matrix data structure to represent zones, which is a state-of-the-art heuristic to improve performance over the classical (and somewhat brute-force) region graph abstraction. The solution provided here is conceptually a marked improvement over some earlier work on the problems [16,9], in which repeated guesses (guided by binary search) and multiple model checking queries were effectively but inelegantly and less efficiently used; here only one run of the zone construction is sufficient to yield the answers. The paper then reports on a prototype implementation of the algorithms using Difference Bound Matrices (DBMs), and presents the results of its application on a realistic automatic manufacturing plant. © 2014 Springer International Publishing Switzerland.