Schedulability Analysis for Timed Automata With Tasks
Schedulability Analysis for Timed Automata With Tasks
复制标题
带任务的定时自动机的可调度性分析
DOI：
10.1145/3477020
复制
发表时间：
2021-09
影响因子：
2
通讯作者：
Wang Yi
中科院分区：
文献类型：
--
作者：
Jinghao Sun;Nan Guan;Rongxiao Shi;Guozhen Tan;Wang Yi
实时计算系统建模与分析的研究主要集中在模型检测和实时调度理论两个方面。在模型检测中，一个有表现力的建模形式主义，如时间自动机（TA）是用来建模复杂的系统，但分析通常是非常昂贵的，由于状态空间爆炸。在实时调度理论中，分析技术是高效的，但模型往往是限制性的。在本文中，我们的目标是利用有效的分析技术的可能性，植根于实时调度理论分析的实时任务系统建模的时间自动机与任务（达特）。更具体地说，我们开发了有效的技术来分析基于TAT的任务模型的可行性（即，是否所有任务都能在单处理器上满足它们的截止期限）使用需求约束函数（DBF），这是实时调度理论中广泛使用的工作负载抽象。我们提出的分析方法具有伪多项式时间复杂度，如果用于建模每个任务的时钟的数量是由一个常数，这是远远低于指数复杂度的传统的基于模型检查的分析方法（也假设时钟的数量是由一个常数）。我们应用动态规划技术来实现基于DBF的分析框架，并提出状态空间修剪技术来加速分析过程。实验结果表明，我们的基于DBF的方法可以分析一个达特系统与50个任务在几分钟内，这显着优于最先进的基于TAT的可扩展性分析工具TIMES。
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.
登录
查看更多内容
DOI：
--
发表时间：
1967
期刊：
--
影响因子：
--
作者：
J. E. Falk;R Fletcher;M. J. D. Powell;Peter E Hart;Nils J Nilsson;Bertram Raphael
通讯作者：
J. E. Falk;R Fletcher;M. J. D. Powell;Peter E Hart;Nils J Nilsson;Bertram Raphael
DOI：
10.1109/ipdps.2003.1213431
发表时间：
2003-04
期刊：
Proceedings International Parallel and Distributed Processing Symposium
影响因子：
--
作者：
Yasmina Abdeddaïm;Abdelkarim Kerbaa;O. Maler
通讯作者：
Yasmina Abdeddaïm;Abdelkarim Kerbaa;O. Maler
DOI：
10.1109/rtss.2005.21
发表时间：
2005-12
期刊：
26th IEEE International Real-Time Systems Symposium (RTSS'05)
影响因子：
--
作者：
S. Chakraborty;L. T. Phan;P. Thiagarajan
通讯作者：
S. Chakraborty;L. T. Phan;P. Thiagarajan
DOI：
10.1016/j.tcs.2005.11.018
发表时间：
2006-03
期刊：
Theor. Comput. Sci.
影响因子：
--
作者：
Yasmina Abdeddaïm;E. Asarin;O. Maler
通讯作者：
Yasmina Abdeddaïm;E. Asarin;O. Maler
DOI：
10.1109/rtss.2010.19
发表时间：
2010-11
期刊：
2010 31st IEEE Real-Time Systems Symposium
影响因子：
--
作者：
Sanjoy Baruah
通讯作者：
Sanjoy Baruah