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

作     者：左正康 赵帅 王昌晶 谢武平 黄箐 

作者机构：江西师范大学数字产业学院 江西师范大学计算机信息工程学院 江西师范大学网络化支撑软件国家科技合作基地 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2024年第10期

页      面：4533-4554页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

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

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

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