基于优先级时间Petri网的实时嵌入式多核系统分析
作者:
作者简介:

张凯文(1995-), 男, 博士生, 主要研究领域为Petri网, 形式化方法, 程序分析. ;刘关俊(1978-), 男, 博士, 教授, 博士生导师, CCF高级会员, 主要研究领域为Petri网, 模型检测, 形式化方法, 机器学习, 人机物系统, 工作流系统, 无人机协同系统. ;孙彦韬(1997-), 男, 博士生, CCF学生会员, 主要研究领域为嵌入式系统, 高性能计算. ;李晓锋(1982-), 男, 研究员, CCF专业会员, 主要研究领域为可信软件, 软件自适应, 智能化软件工程. ;关健(1986-), 女, 高级工程师, 主要研究领域为人工智能软件, 嵌入式系统. ;解毅(1994-), 男, 工程师, 主要研究领域为嵌入式系统. ;顾斌(1968-), 男, 博士, 研究员, 博士生导师, CCF高级会员, 主要研究领域为可信软件, 计算机控制, 嵌入式软件.

通讯作者:

刘关俊, Email: liuguanjun@tongji.edu.cn;李晓锋, E-mail: li_x_feng@126.com

中图分类号:

TP311

基金项目:

国家自然科学基金(62172299, 62192730, 62032019); 北京控制工程研究所高可信嵌入式软件工程技术实验室开放基金(LHCESET202201); 北京控制工程研究所空间光电测量与感知实验室开放基金(LabSOMP-2023-03); CCF-华为胡杨林基金-形式化专项(CCF-HuaweiFM202305)


Analysis of Real-time Embedded Multi-core System Based on Prioritized Time Petri Net
Author:
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [32]
  • |
  • 相似文献 [20]
  • | | |
  • 文章评论
    摘要:

    已有的基于点区间优先级时间Petri网分析实时嵌入式多核系统的工作, 存在以下不足: (1)点区间优先级时间Petri网只考虑每个任务的执行时间是一个固定值的情况, 而更多的实际应用中每个任务的执行时间是在一个区间范围内, 因此不能模拟这些应用; (2)没有实现从任务依赖图到点区间优先级时间Petri网的自动转化, 不便于工程设计人员使用; (3)没有考虑任务间互斥访问共享变量的情况. 为此, 定义了优先级时间Petri网(Pri-TPN)以弥补第1个不足; 定义带有资源分配与优先级的任务依赖图(TDG-RAP)以弥补第3个不足; 给出从TDG-RAP到Pri-TPN的转化规则与算法以弥补第2个不足, 以及基于Pri-TPN分析任务最坏执行时间与系统死锁的算法; 开发工具软件, 方便工程设计人员使用.

    Abstract:

    Existing work on the analysis of real-time embedded multi-core systems using point-interval prioritized time Petri nets has the following limitations. (1) Point-interval prioritized time Petri nets only consider the case where the execution time of each task is a fixed value, but in many practical applications, the execution time of a task is generally within a range so that this kind of model cannot be used to analyze these applications. (2) There is a lack of automatic transformation from task dependency graphs to this point-interval prioritized time Petri nets, and thus it is inconvenient for engineering designers. (3) The case of mutually exclusive access to shared variables has not been considered. To address these issues, this study defines prioritized time Petri nets (Pri-TPN) to overcome the first limitation and introduces a task dependency graph with resource allocation and priority (TDG-RAP) to overcome the third limitation. It develops algorithms based on Pri-TPN for analyzing the worst-case execution time (WCET) and system deadlocks of tasks. Additionally, a tool software is developed to facilitate its use by engineering designers.

    参考文献
    [1] Cousot P, Cousot R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of the 4th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages. Los Angeles: ACM, 1977. 238–252. [doi: 10.1145/512950.512973]
    [2] Li YTS, Malik S. Performance analysis of embedded software using implicit path enumeration. In: Proc. of the 32nd Design Automation Conf. San Francisco: IEEE, 1995. 456–461. [doi: 10.1109/DAC.1995.249991]
    [3] Rochange C. Parallel real-time tasks, as viewed by WCET analysis and task scheduling approaches. In: Proc. of the 16th Int’l Workshop on Worst-case Execution Time Analysis (WCET 2016). Open Access Series in Informatics (OASIcs), Vol. 55. 11:1–11:11.
    [4] Melani A, Bertogna M, Bonifaci V, Marchetti-Spaccamela A, Buttazzo GC. Response-time analysis of conditional DAG tasks in multiprocessor systems. In: Proc. of the 27th Euromicro Conf. on Real-time Systems. Lund: IEEE, 2015. 211–221.
    [5] 王戟, 詹乃军, 冯新宇, 刘志明. 形式化方法概貌. 软件学报, 2019, 30(1): 33–61. http://www.jos.org.cn/1000-9825/5652.htm
    Wang J, Zhan NJ, Feng XY, Liu ZY. 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
    [6] 崔进, 段振华, 田聪, 张南. 一种嵌套中断系统的建模和分析方法. 软件学报, 2018, 29(6): 1670–1680. http://www.jos.org.cn/1000-9825/5472.htm
    Cui J, Duan ZH, Tian C, Zhang N. Modeling and analysis of nested interrupt systems. Ruan Jian Xue Bao/Journal of Software, 2018, 29(6): 1670–1680 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5472.htm
    [7] Clarke Jr EM, Grumberg O, Kroening D, Peled D, Veith H. Model Checking. 2nd ed., Cambridge: MIT Press, 2018.
    [8] Wang C, Feng XJ, Li X, Zhou XH, Chen P. Colored Petri net model with automatic parallelization on real-time multicore architectures. Journal of Systems Architecture, 2014, 60(3): 293–304.
    [9] Huang B, Zhou MC, Lu XS, Abusorrah A. Scheduling of resource allocation systems with timed Petri nets: A survey. ACM Computing Surveys, 2023, 55(11): 230.
    [10] Cui J, Duan ZH, Tian C, Du HW. A novel approach to modeling and verifying real-time systems for high reliability. IEEE Trans. on Reliability, 2018, 67(2): 481–493.
    [11] Zhong WJ, Zhou JT, Sun T. Concurrent software fine-coarse-grained automatic modelling by coloured Petri nets for model checking. IET Software, 2023, 17(1): 55–75.
    [12] 董威, 王戟, 齐治昌. 并发和实时系统的模型检验技术. 计算机研究与发展, 2001, 38(6): 698–705.
    Dong W, Wang J, Qi ZC. Model checking for concurrent and real-time systems. Journal of Computer Research and Development, 2001, 38(6): 698–705 (in Chinese with English abstract).
    [13] 何雷锋, 刘关俊. 模拟实时系统的点区间优先级时间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
    [14] Liu GJ, Jiang CJ, Zhou MC. Time-soundness of time Petri nets modelling time-critical systems. ACM Trans. on Cyber-physical Systems, 2018, 2(2): 11.
    [15] 刘关俊. Petri网的元展: 一种并发系统模型检测方法. 北京: 科学出版社, 2020.
    Liu GJ. Primary Unfolding of Petri Nets: A Model Checking Method for Concurrent Systems. Beijing: Science Press, 2020 (in Chinese).
    [16] Fauzan AC, Sarno R, Yaqin MA. Performance measurement based on coloured Petri net simulation of scalable business processes. In: Proc. of the 4th Int’l Conf. on Electrical Engineering, Computer Science and Informatics. Yogyakarta: IEEE, 2017. 1?6.
    [17] Lime D, Roux OH. Expressiveness and analysis of scheduling extended time Petri nets. IFAC Proc. Volumes, 2003, 36(13): 189–197.
    [18] 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. [doi: 10.1109/EMRTS.2003.1212753]
    [19] Bucci G, Fedeli A, Sassoli L, Vicario E. Timed state space analysis of real-time preemptive systems. IEEE Trans. on Software Engineering, 2004, 30(2): 97–111.
    [20] Roux OH, Lime D. Time Petri nets with inhibitor hyperarcs. Formal semantics and state space computation. In: Proc. of the 2004 Int’l Conf. on Application and Theory of Petri Nets. Bologna: Springer, 2004. 371?390. [doi: 10.1007/978-3-540-27793-4_21]
    [21] 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.
    [22] Liu F, Zhang HM. A class of extended time Petri nets for modeling and simulation of discrete event systems. Simulation, 2018, 94(8): 753–762.
    [23] Lu FM, Tao RR, Du YY, Zeng QT, Bao YX. Deadlock detection-oriented unfolding of unbounded Petri nets. Information Sciences, 2019, 497: 1?22. [doi: 10.1016/j.ins.2019.05.021]
    [24] Roux OH, Déplanche AM. A T-time Petri net extension for real time-task scheduling modeling. European Journal of Automation, 2002, 36(7): 973–987.
    [25] van der Aalst WMP. The application of Petri nets to workflow management. Journal of Circuits, Systems and Computers, 1998, 8(1): 21–66.
    [26] Liu GJ. Petri Nets: Theoretical Models and Analysis Methods for Concurrent Systems. Singapore: Springer, 2022. [doi: 10.1007/978-981-19-6309-4]
    [27] Haur I, Béchennec JL, Roux OH. High-level colored time Petri nets for true concurrency modeling in real-time software. In: Proc. of the 8th Int’l Conf. on Control, Decision and Information Technologies (CoDIT). Istanbul: IEEE, 2022. 21–26.
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

张凯文,刘关俊,孙彦韬,李晓锋,关健,解毅,顾斌.基于优先级时间Petri网的实时嵌入式多核系统分析.软件学报,2024,35(9):4123-4140

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

京公网安备 11040202500063号