Finding Best and Worst Case Execution Times of Systems Using Difference-Bound Matrices
- 499 Downloads
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.
KeywordsExecution Time Model Check Symbolic State Clock Constraint Clock Variable
Unable to display preview. Download preview PDF.
- 1.Alur, R., Dill, D.: A theory of timed automata. TCS, 183–235 (1994)Google Scholar
- 2.Behrmann, G., Bouyer, P., Larsen, K.G., Radek, P.: Lower and upper bounds in zone-based abstractions of timed automata. Int. J. Softw. Tools Technol. Transf., 204–215 (2006)Google Scholar
- 8.Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press (2001)Google Scholar
- 9.Dalsgaard, A.E., Olesen, M.C., Toft, M., Hansen, R.R., Larsen, K.G.: METAMOC: Modular Execution Time Analysis using Model Checking. In: WCET 2010, pp. 113–123 (2010)Google Scholar
- 11.Daws, C., Yovine, S.: Two examples of verification of multirate timed automata with kronos. In: Proceedings of the 16th IEEE Real-Time Systems Symposium, RTSS 1995. IEEE Computer Society (1995)Google Scholar
- 12.Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, pp. 197–212. Springer-Verlag New York, Inc. (1990)Google Scholar
- 13.Floyd, R.W.: Algorithm 97: Shortest path. Communications of the ACM (1962)Google Scholar
- 14.Herbreteau, F., Kini, D., Srivathsan, B., Walukiewicz, I.: Using non-convex approximations for efficient analysis of timed automata. In: FSTTCS (2011)Google Scholar
- 17.Rokicki, T.G.: Representing and Modeling Digital Circuits. PhD thesis, Stanford University (1993)Google Scholar