模拟实时系统的点区间优先级时间 Petri 网与 TCTL 验证
2022-10-27 20:56:19   来源：    点击：

摘要:时间Petri网为实时系统提供了一种形式化的建模方法，时间计算树逻辑(TCTL)为描述实时系统与时间相关的设计需求提供了一种逻辑化的表达方式，因此，基于时间Petri 网的TCTL模型检测广泛应用于实时系统的正确性验证.然而对于一些涉及优先级的实时系统，例如多核多任务实时系统，这里不仅需要考虑任务之间的时间约束,还要考虑任务执行的优先级以及引入优先级带来的抢占式调度问题,致使相应的建模和分析变得更加困难.为此,提出了点区间优先级时间Petri 网，通过在时间Petri网上定义变迁发生的优先级以及变迁的可挂起性,从而可以模拟实时系统的抢占式调度机制.首先，高优先级的任务抢占低优先级的任务所占用的资源，导致后者被中断;然后，前者执行完毕后释放资源;最后，后者再次获得资源，从中断的地方恢复.通过点区间优先级时间Petri网来模拟多核多任务实时系统,使用TCTL来描述它们的设计需求,设计了相应的模型检测算法，开发了相应的模型检测器以验证它们的正确性.通过一个实例，来说明该模型和方法的有效性.