Beyond Liveness: Efficient Parameter Synthesis for Time Bounded Liveness
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  for general parameterised TCTL using a translation to Presburger arithmetic and also considered by F. Wang in  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  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.
- 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
- 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