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

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

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

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,this study proposes 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.This study uses time-point-interval prioritized time Petri nets to model multi-core multi-task real-time systems,uses TCTL to describe their design requirements,designs the corresponding model checking algorithms,and develops the corresponding model checker to verify their correctness.An example is used to show the effectiveness of the proposed model and method.