抢占式调度问题的PPTA模型与验证方法
作者:
作者简介:

左正康(1980-), 男, 博士, 副教授, CCF高级会员, 主要研究领域为形式化方法, 智能化软件;赵帅(1999-), 男, 硕士生, 主要研究领域为模型检测, 形式化方法;王昌晶(1977-), 男, 博士, 教授, 博士生导师, CCF高级会员, 主要研究领域为高可信软件, 智能化软件;谢武平(1984-), 男, 博士, 讲师, CCF专业会员, 主要研究领域为形式化方法, 可信软件;黄箐(1984-), 男, 博士, 副教授, CCF专业会员, 主要研究领域为智能化软件

通讯作者:

谢武平, E-mail: wupingxie@jxnu.edu.cn

中图分类号:

TP311

基金项目:

国家自然科学基金(61862033, 62262031); 江西省教育厅科技项目(GJJ210307, GJJ210334)


PPTA Model and Verification Method for Preemptive Scheduling Problem
Author:
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [33]
  • |
  • 相似文献 [20]
  • | | |
  • 文章评论
    摘要:

    优先级用于解决诸如在资源共享和安全设计等方面的冲突, 已经成为实时系统设计中不可或缺的一部分. 对于引入优先级的实时系统, 每个任务都会被分配优先级, 这就导致低优先级的任务在运行时可能会被高优先级的任务抢占资源, 进而给实时系统带来抢占式调度问题. 现有研究, 缺乏一种可以直观表示任务的优先级以及任务之间的依赖关系的建模及自动验证方法. 为此, 提出抢占式优先级时间自动机(PPTA)并引入抢占式优先级时间自动机网络(PPTAN). 首先, 通过在时间自动机上添加变迁的优先级来表示任务的优先级, 再利用变迁将具有依赖关系的任务相关联, 从而可以利用PPTA建模带有优先级的实时任务. 在时间自动机上添加阻塞位置, 进而利用PPTAN建模优先级抢占式调度问题. 其次, 提出基于模型的转换方法, 将抢占式优先级时间自动机映射到自动验证工具UPPAAL中. 最后, 通过建模多核多任务实时系统实例并与其他模型进行对比, 说明所提模型不仅适用于建模优先级抢占式调度问题并可对其进行准确验证分析.

    Abstract:

    As an essential component of real-time system design, priority is utilized to resolve conflicts in resource sharing and design for safety. For real-time systems that introduce priorities, each task is assigned a priority, which leads to the possibility of low-priority tasks being preempted by high-priority tasks at runtime, thus creating a preemptive scheduling problem for real-time systems. Existing research on this problem lacks a modeling and automatic verification method that can visually represent the priority of tasks and the dependencies between tasks. To this end, a preemptive priority timed automata (PPTA) is proposed and a preemptive priority timed automata network (PPTAN) is introduced. First, the priority of a task is represented by adding the priority of migration to the timed automata, and then the migration is adopted to correlate tasks with dependencies so that PPTA can be applied to model real-time tasks with priority. The blocking position is also added to the timed automata, so PPTAN can be used to model the priority preemptive scheduling problem. Second, a model-based transformation method is proposed to map the PPTA to the automatic verification tool UPPAAL. Finally, by modeling an example of a multi-core multi-task real-time system and comparing it with other models, it is shown that this model is not only suitable for modeling the priority preemptive scheduling problem but also for accurately verifying and analyzing it.

    参考文献
    [1] Sun JH, Guan N, Shi RX, Tan GZ, Yi W. Schedulability analysis for timed automata with tasks. ACM Transactions on Embedded Computing Systems, 2021, 20(5s): 89. [doi: 10.1145/3477020]
    [2] Copic M, Leupers R, Ascheid G. Efficient sporadic task handling in parallel AUTOSAR applications using runnable migration. In: Proc. of the 24th Asia and South Pacific Design Automation Conf. Tokyo: Association for Computing Machinery, 2019. 603–608.
    [3] Dai XT, Zhao S, Jiang Y, Jiao X, Hu XS, Chang WL. Fixed-priority scheduling and controller co-design for time-sensitive networks. In: Proc. of the 2020 IEEE/ACM Int’l Conf. on Computer Aided Design (ICCAD). San Diego: IEEE, 2020. 1–9.
    [4] Wang DG, Wang X, Li ZW. Nonblocking supervisory control of state-tree structures with conditional-preemption matrices. IEEE Transactions on Industrial Informatics, 2020, 16(6): 3744–3756. [doi: 10.1109/TII.2019.2939628]
    [5] 刘纯尧, 张立臣. 信息物理融合系统的动态多优先级调度. 计算机科学, 2015, 42(1): 28–32. [doi: 10.11896/j.issn.1002-137X.2015.1.006]
    Liu CY, Zhang LC. Dynamic multi-priority scheduling for cyber-physical systems. Computer Science, 2015, 42(1): 28–32 (in Chinese with English abstract). [doi: 10.11896/j.issn.1002-137X.2015.1.006]
    [6] 何雷锋, 刘关俊. 模拟实时系统的点区间优先级时间Petri网与TCTL验证. 软件学报, 2022, 33(8): 2947–2963. http://www.jos.org.cn/1000-9825/6607.htm
    He LF, Liu GJ. Time-point-interval prioritized time Petri nets modelling real-time systems and TCTL checking. Ruan Jian Xue Bao/Journal of Software, 2022, 33(8): 2947–2963 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6607.htm
    [7] 王戟, 詹乃军, 冯新宇, 刘志明. 形式化方法概貌. 软件学报, 2019, 30(1): 33–61. http://www.jos.org.cn/1000-9825/5652.htm
    Wang J, Zhan NJ, Feng XY, Liu ZM. Overview of formal methods. Ruan Jian Xue Bao/Journal of Software, 2019, 30(1): 33–61 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5652.htm
    [8] Berthomieu B, Diaz M. Modeling and verification of time dependent systems using time Petri nets. IEEE Transactions on Software Engineering, 1991, 17(3): 259–273. [doi: 10.1109/32.75415]
    [9] Alur R, Dill DL. A theory of timed automata. Theoretical Computer Science, 1994, 126(2): 183–235. [doi: 10.1016/0304-3975(94)90010-8]
    [10] Berthomieu B, Peres F, Vernadat F. Model checking bounded prioritized time Petri nets. In: Proc. of the 5th Int’l Symp. on Automated Technology for Verification and Analysis. Tokyo: Springer, 2007. 523–532.
    [11] Lime D, Roux OH. Expressiveness and analysis of scheduling extended time Petri nets. IFAC Proceedings Volumes, 2003, 36(13): 189–197. [doi: 10.1016/S1474-6670(17)32483-7]
    [12] Bucci G, Fedeli A, Sassoli L, Vicario E. Modeling flexible real time systems with preemptive time Petri nets. In: Proc. of the 15th Euromicro Conf. on Real-time Systems. Porto: IEEE, 2003. 279–286.
    [13] Roux OH, Lime D. Time Petri nets with inhibitor hyperarcs. Formal semantics and state space computation. In: Proc. of the 25th Int’l Conf. on Application and Theory of Petri Nets. Bologna: Springer, 2004. 371–390.
    [14] Berthomieu B, Lime D, Roux OH, Vernadat F. Reachability problems and abstract state spaces for time Petri nets with stopwatches. Discrete Event Dynamic Systems, 2007, 17(2): 133–158. [doi: 10.1007/s10626-006-0011-y]
    [15] David A, Illum J, Larsen KG, Skou A. Model-based framework for schedulability analysis using UPPAAL 4.1. In: Nicolescu G, Mosterman PJ, eds. Model-based Design for Embedded Systems. Boca Raton: CRC Press, 2010. 93–119.
    [16] Lin SW, Hsiung PA. Model checking prioritized timed systems. IEEE Transactions on Computers, 2012, 61(6): 843–856. [doi: 10.1109/TC.2011.99]
    [17] Behrmann G, David A, Larsen KG. A tutorial on UPPAAL. In: Proc. of the 2004 Formal Methods for the Design of Real-time Systems: Int’l School on Formal Methods for the Design of Computer, Communication, and Software Systems. Bertinoro: Springer, 2004. 200–236.
    [18] Clarke EM, Emerson EA, Sistla AP. Automatic verification of finite state concurrent system using temporal logic specifications: A practical approach. In: Proc. of the 10th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages. Austin: Association for Computing Machinery, 1983. 117–126.
    [19] 张广泉. 形式化方法导论. 北京: 清华大学出版社, 2015.
    Zhang GQ. Introduction to Formal Methods. Beijing: Tsinghua University Press, 2015 (in Chinese).
    [20] 陈小颖, 祝义, 赵宇, 王金永. 面向CPS时空性质验证的混成AADL建模与模型转换方法. 软件学报, 2021, 32(6): 1779–1798. http://www.jos.org.cn/1000-9825/6249.htm
    Chen XY, Zhu Y, Zhao Y, Wang JY. Hybrid AADL modeling and model transformation for CPS time and space properties verification. Ruan Jian Xue Bao/Journal of Software, 2021, 32(6): 1779–1798 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6249.htm
    [21] Clarke EM, Emerson EA, Sifakis J. Model checking: Algorithmic verification and debugging. Communications of the ACM, 2009, 52(11): 74–84. [doi: 10.1145/1592761.1592781]
    [22] 王淑灵, 詹博华, 盛欢欢, 吴昊, 易士程, 王令泰, 金翔宇, 薛白, 李静辉, 向霜晴, 向展, 毛碧飞. 可信系统性质的分类和形式化研究综述. 软件学报, 2022, 33(7): 2367–2410. http://www.jos.org.cn/1000-9825/6587.htm
    Wang SL, Zhan BH, Sheng HH, Wu H, Yi SC, Wang LT, Jin XY, Xue B, Li JH, Xiang SQ, Xiang Z, Mao BF. Survey on requirements classification and formalization of trustworthy systems. Ruan Jian Xue Bao/Journal of Software, 2022, 33(7): 2367–2410 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6587.htm
    [23] 代声馨, 洪玫, 郭兵, 杨秋辉, 黄蔚, 徐保平. 多处理器实时系统可调度性分析的UPPAAL模型. 软件学报, 2015, 26 (2): 279–296. http://www.jos.org.cn/1000-9825/4781.htm
    Dai SX, Hong M, Guo B, Yang QH, Huang W, Xu BP. Schedulability analysis model for multiprocessor real-time systems using UPPAAL. Ruan Jian Xue Bao/Journal of Software, 2015, 26(2): 279–296 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4781.htm
    [24] 赵旭辉, 庄雷. 一种基于优先级扩展的时间自动机模型中DBM减法算法的改进. 计算机工程与科学, 2008, 30(11): 56–59. [doi: 10.3969/j.issn.1007-130X.2008.11.018]
    Zhao XH, Zhuang L. Improvement on a DBM subtraction algorithm in timed automata with priorities. Computer Engineering & Science, 2008, 30(11): 56–59 (in Chinese with English abstract). [doi: 10.3969/j.issn.1007-130X.2008.11.018]
    [25] Pimkote A, Vatanawood W. Simulation of preemptive scheduling of the independent tasks using timed automata. In: Proc. of the 10th Int’l Conf. on Software and Computer Applications. Kuala Lumpur: Association for Computing Machinery, 2021. 7–13.
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

左正康,赵帅,王昌晶,谢武平,黄箐.抢占式调度问题的PPTA模型与验证方法.软件学报,2024,35(10):4533-4554

复制
分享
文章指标
  • 点击次数:725
  • 下载次数: 2634
  • HTML阅读次数: 1074
  • 引用次数: 0
历史
  • 收稿日期:2022-12-20
  • 最后修改日期:2023-03-14
  • 在线发布日期: 2023-09-06
  • 出版日期: 2024-10-06
文章二维码
您是第20652424位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号