Beyond Liveness: Efficient Parameter Synthesis for Time Bounded Liveness

  • Gerd Behrmann
  • Kim G. Larsen
  • Jacob Illum Rasmussen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3829)


In this paper, we deal with the problem of parameter synthesis for a subset of parameterised TCTL over timed automata. The problem was proved decidable by V. Bruyere et al. in [10] for general parameterised TCTL using a translation to Presburger arithmetic and also considered by F. Wang in [13] using a parametric region construction. In contrast, we provide two efficient zone based algorithms for a useful subset of parameterised TCTL. The subset has obvious applications to worst case execution time (WCET) analysis. In [11] WCET is performed via model checking, but their approach uses a binary search strategy over several invocations of the model checker. In contrast, both our algorithms synthesise the bound directly. We provide experimental results based on a prototype implementation in Uppaal for two case studies: The first concerns response time analysis of a well known train gate scenario. The second is an execution time analysis of task graph problems where tasks have uncertain execution times.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Courcoubetis, C., Dill, D.: Model-checking for real-time systems. In: Proc. 5th IEEE Symposium on Logic in Computer Science (LICS 1990), pp. 414–425. IEEE Computer Society Press, Los Alamitos (1990)CrossRefGoogle Scholar
  2. 2.
    Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science (TCS) 126(2), 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static guard analysis in timed automata verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 254–277. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  4. 4.
    Behrmann, G., Bouyer, P., Larsen, K.G., Pelanek, R.: Lower and upper bounds in zone based abstractions of timed automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 312–326. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  5. 5.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, Springer, Heidelberg (2004)CrossRefGoogle Scholar
  6. 6.
    Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.: 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
  7. 7.
    Bouajjani, A., Tripakis, S., Yovine, S.: On-the-fly symbolic model-checking for real-time systems. In: Proc. 18th IEEE Real-Time Systems Symposium (RTSS 1997), pp. 25–35. IEEE Computer Society Press, Los Alamitos (1997)Google Scholar
  8. 8.
    Bouyer, P.: Untameable timed automata? In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 620–631. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  9. 9.
    Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: a model-checking tool for real-time systems. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 546–550. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  10. 10.
    Bruyère, V., Dall’Olio, E., Raskin, J.-F.: Durations, parametric model-checking in timed automata with presburger arithmetic. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 687–698. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  11. 11.
    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
  12. 12.
    Tobita, T., Kouda, M., Kasahara, H.: Performance evaluation of minimum execution time multiprocessor scheduling algorithms using standard task graph set. In: Proc. of PDPTA 2000, pp. 745–751 (2000)Google Scholar
  13. 13.
    Wang, F.: Parametric analysis of computer systems. Journal of Formal Methods in Systems Design 17, 39–60 (2000)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Gerd Behrmann
    • 1
  • Kim G. Larsen
    • 1
  • Jacob Illum Rasmussen
    • 1
  1. 1.Department of Computer ScienceAalborg UniversityDenmark

Personalised recommendations