首页> 外文会议>2011 23rd Euromicro Conference on Real-Time Systems >Modelling, Verification and Synthesis of Two-Tier Hierarchical Fixed-Priority Preemptive Scheduling
【24h】

Modelling, Verification and Synthesis of Two-Tier Hierarchical Fixed-Priority Preemptive Scheduling

机译:两层分层固定优先级抢占式调度的建模,验证和综合

获取原文

摘要

Hierarchical scheduling has major benefits when it comes to integrating hard real-time applications. One of those benefits is that it gives a clear runtime separation of applications in the time domain. This in turn gives a protection against timing error propagation in between applications. However, these benefits rely on the assumption that the scheduler itself schedules applications correctly according to the scheduling parameters and the chosen scheduling policy. A faulty scheduler can affect all applications in a negative way. Hence, being able to guarantee that the scheduler is correct is of great importance. Therefore, in this paper, we study how properties of hierarchical scheduling can be verified. We model a hierarchically scheduled system using task automata, and we conduct verification with model checking using the Times tool. Further, we generate C-code from the model and we execute the hierarchical scheduler in the Vx Works kernel. The CPU and memory overhead of the modelled scheduler is compared against an equivalent manually coded two-level hierarchical scheduler. We show that the worst-case memory consumption is similar and that there is a considerable difference in CPU overhead.
机译:在集成硬实时应用程序时,分层调度具有重大优势。这些好处之一是,它可以在时域中对应用程序进行清晰的运行时分离。反过来,这可以防止应用程序之间的时序误差传播。但是,这些好处依赖于这样的假设,即调度程序本身会根据调度参数和所选的调度策略正确地调度应用程序。错误的调度程序可能会对所有应用程序产生负面影响。因此,能够保证调度程序正确是非常重要的。因此,在本文中,我们研究如何验证分层调度的属性。我们使用任务自动机对分层计划的系统进行建模,并使用Times工具对模型检查进行验证。此外,我们从模型生成C代码,并在Vx Works内核中执行分层调度程序。将建模的调度程序的CPU和内存开销与等效的手动编码的两级分层调度程序进行比较。我们表明,最坏情况下的内存消耗是相似的,并且CPU开销有相当大的差异。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号