模拟实时系统的点区间优先级时间Petri网与TCTL验证

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

Time-point-interval Prioritized Time Petri Nets Modelling Real-time Systems and TCTL Checking

Time Petri nets is a formal method for modelling real-time systems, and Timed Computation Tree Logic (TCTL) is a logical expression for specifying time-related design requirements of real-time systems, so time Petri net based TCTL model checking has been widely used to verify the correction of real-time systems. For those real-time systems with priority such as multi-core multi-task real-time systems, it not only needs to consider time constraints among tasks but also needs to consider priority of task execution and the preemptive scheduling problem caused by priority, which results that modelling and analysis of these systems become more difficult. Therefore, in this paper we propose time-point-interval prioritized time Petri nets. By defining priority of transition firing and suspendable transitions in time Petri nets, time-point-interval prioritized time Petri nets can model preemptive scheduling of real-time systems, i.e., first of all, a high-priority task preempts the resource of a low-priority task, which results in the interruption of the latter, then the former is completed and releases the resource, and finally the latter gets the resource again and resumes from the interruption. In this paper, we use time-point-interval prioritized time Petri nets to model multi-core multi-task real-time systems, use TCTL to describe their design requirements, design the corresponding model checking algorithms, and develop the corresponding model checker to verify their correctness. We use an example to show the effectiveness of our model and method.