Research on modeling and analysis of real-time computing systems has been done in two areas, model checking and real-time scheduling theory. In model checking, an expressive modeling formalism such as timed automata (TA) is used to model complex systems, but the analysis is typically very expensive due to state-space explosion. In real-time scheduling theory, the analysis techniques are highly efficient, but the models are often restrictive. In this paper, we aim to exploit the possibility of applying efficient analysis techniques rooted in real-time scheduling theory to analysis of real-time task systems modeled by timed automata with tasks (TAT). More specifically, we develop efficient techniques to analyze the feasibility of TAT-based task models (i.e., whether all tasks can meet their deadlines on single-processor) using demand bound functions (DBF), a widely used workload abstraction in real-time scheduling theory. Our proposed analysis method has a pseudo-polynomial time complexity if the number of clocks used to model each task is bounded by a constant, which is much lower than the exponential complexity of the traditional model-checking based analysis approach (also assuming the number of clocks is bounded by a constant). We apply dynamic programming techniques to implement the DBF-based analysis framework, and propose state space pruning techniques to accelerate the analysis process. Experimental results show that our DBF-based method can analyze a TAT system with 50 tasks within a few minutes, which significantly outperforms the state-of-the-art TAT-based schedulability analysis tool TIMES.

The demand bound function (DBF) is a powerful abstraction to analyze the feasibility/schedulability of real-time tasks. Computing the DBF for expressive system models, such as graph-based tasks, is typically very expensive. In this article, we develop new techniques to drastically improve the DBF computation efficiency for a representative graph-based task model, digraph real-time tasks (DRT). First, we apply the well-known quick processor-demand analysis (QPA) technique, which was originally designed for simple sporadic tasks, to the analysis of DRT. The challenge is that existing analysis techniques of DRT have to compute the demand for each possible interval size, which is contradictory to the idea of QPA that aims to aggressively skip the computation for most interval sizes. To solve this problem, we develop a novel integer linear programming (ILP)-based analysis technique for DRT, to which we can apply QPA to significantly improve the analysis efficiency. Second, we improve the task utilization computation (a major step in DBF computation for DRT) efficiency from pseudo-polynomial complexity to polynomial complexity. Experiments show that our approach can improve the analysis efficiency by dozens of times.