典型文献
模拟实时系统的点区间优先级时间Petri网与TCTL验证
文献摘要:
时间Petri网为实时系统提供了一种形式化的建模方法,时间计算树逻辑(TCTL)为描述实时系统与时间相关的设计需求提供了一种逻辑化的表达方式,因此,基于时间Petri网的TCTL模型检测广泛应用于实时系统的正确性验证.然而对于一些涉及优先级的实时系统,例如多核多任务实时系统,这里不仅需要考虑任务之间的时间约束,还要考虑任务执行的优先级以及引入优先级带来的抢占式调度问题,致使相应的建模和分析变得更加困难.为此,提出了点区间优先级时间Petri网,通过在时间Petri网上定义变迁发生的优先级以及变迁的可挂起性,从而可以模拟实时系统的抢占式调度机制.首先,高优先级的任务抢占低优先级的任务所占用的资源,导致后者被中断;然后,前者执行完毕后释放资源;最后,后者再次获得资源,从中断的地方恢复.通过点区间优先级时间Petri网来模拟多核多任务实时系统,使用TCTL来描述它们的设计需求,设计了相应的模型检测算法,开发了相应的模型检测器以验证它们的正确性.通过一个实例,来说明该模型和方法的有效性.
文献关键词:
点区间优先级时间Petri网;多核多任务实时系统;时间计算树逻辑(TCTL);模型检测;抢占式调度
中图分类号:
作者姓名:
何雷锋;刘关俊
作者机构:
同济大学 计算机科学与技术系, 上海 201804
文献出处:
引用格式:
[1]何雷锋;刘关俊-.模拟实时系统的点区间优先级时间Petri网与TCTL验证)[J].软件学报,2022(08):2947-2963
A类:
TCTL,多核多任务实时系统,抢占式调度
B类:
Petri,形式化,设计需求,表达方式,模型检测,正确性验证,时间约束,调度问题,挂起,调度机制,高优,低优先级,完毕,检测算法,检测器
AB值:
0.142903
相似文献
机标中图分类号,由域田数据科技根据网络公开资料自动分析生成,仅供学习研究参考。