抢占式调度问题的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:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    优先级用于解决诸如在资源共享和安全设计等方面的冲突, 已经成为实时系统设计中不可或缺的一部分. 对于引入优先级的实时系统, 每个任务都会被分配优先级, 这就导致低优先级的任务在运行时可能会被高优先级的任务抢占资源, 进而给实时系统带来抢占式调度问题. 现有研究, 缺乏一种可以直观表示任务的优先级以及任务之间的依赖关系的建模及自动验证方法. 为此, 提出抢占式优先级时间自动机(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.

    参考文献
    相似文献
    引证文献
引用本文

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

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

京公网安备 11040202500063号