Finding Best and Worst Case Execution Times of Systems Using Difference-Bound Matrices

  • Omar Al-Bataineh
  • Mark Reynolds
  • Tim French
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8711)


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.


Execution Time Model Check Symbolic State Clock Constraint Clock Variable 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Dill, D.: A theory of timed automata. TCS, 183–235 (1994)Google Scholar
  2. 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
  3. 3.
    Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.: Efficient Guiding Towards Cost-Optimality in UPPAAL. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 174–188. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  4. 4.
    Behrmann, G., Larsen, K.G., Rasmussen, J.I.: Beyond liveness: Efficient parameter synthesis for time bounded liveness. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 81–94. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  5. 5.
    Bengtsson, J.E., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  6. 6.
    Bouyer, P.: Forward analysis of updatable timed automata. Form. Methods Syst. Des. 24, 281–320 (2004)CrossRefzbMATHGoogle Scholar
  7. 7.
    Bryans, J., Bowman, H., Derrick, J.: Model checking stochastic automata. ACM Transactions on Computational Logic (TOCL) 4(4), 452–492 (2003)CrossRefMathSciNetGoogle Scholar
  8. 8.
    Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press (2001)Google Scholar
  9. 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
  10. 10.
    Dalsgaard, A.E., Hansen, R.R., Jørgensen, K.Y., Larsen, K.G., Olesen, M.C., Olsen, P., Srba, J.: opaal: A lattice model checker. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 487–493. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  11. 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. 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. 13.
    Floyd, R.W.: Algorithm 97: Shortest path. Communications of the ACM (1962)Google Scholar
  14. 14.
    Herbreteau, F., Kini, D., Srivathsan, B., Walukiewicz, I.: Using non-convex approximations for efficient analysis of timed automata. In: FSTTCS (2011)Google Scholar
  15. 15.
    Horváth, A., Paolieri, M., Ridi, L., Vicario, E.: Transient analysis of non-markovian models using stochastic state classes. Performance Evaluation 69(7), 315–335 (2012)CrossRefGoogle Scholar
  16. 16.
    Metzner, A.: Why model checking can improve WCET analysis. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 334–347. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  17. 17.
    Rokicki, T.G.: Representing and Modeling Digital Circuits. PhD thesis, Stanford University (1993)Google Scholar
  18. 18.
    Traonouez, L.-M., Lime, D., Roux, O.H.: Parametric model-checking of time petri nets with stopwatches using the state-class graph. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 280–294. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  19. 19.
    Wilhelm, R.: Why AI + ILP is good for WCET, but MC is not, nor ILP alone. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 309–322. Springer, Heidelberg (2004)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Omar Al-Bataineh
    • 1
  • Mark Reynolds
    • 1
  • Tim French
    • 1
  1. 1.The University of Western AustraliaPerthAustralia

Personalised recommendations