抢占式调度问题的PPTA模型与验证方法  

PPTA Model and Verification Method for Preemptive Scheduling Problem

作　　者：左正康[1,2] 赵帅 王昌晶[1,2] 谢武平[3] 黄箐 ZUO Zheng-Kang;ZHAO Shuai;WANG Chang-Jing;XIE Wu-Ping;HUANG Qing(School of Digital Industry,Jiangxi Normal University,Shangrao 334006,China;School of Computer and Information Engineering,Jiangxi Normal University,Nanchang 330022,China;National-level International S&T Cooperation Base of Networked Supporting Software,Jiangxi Normal University,Nanchang 330022,China)

机构地区：[1]江西师范大学数字产业学院,江西上饶334006 [2]江西师范大学计算机信息工程学院,江西南昌330022 [3]江西师范大学网络化支撑软件国家科技合作基地,江西南昌330022

出　　处：《软件学报》2024年第10期4533-4554,共22页Journal of Software

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

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

关 键 词：优先级抢占式调度 抢占式优先级时间自动机 多核多任务实时系统 UPPAAL 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]