Prioritized Time-Point-Interval Petri Nets Modeling Multiprocessor Real-Time Systems and TCTLx

When a group of real-time tasks with dependent relations are performed in parallel in a multiprocessor interruptible environment, time-related requirements are easily destroyed so that the correct design of such a system is complex and difficult. Therefore, it is necessary for designers to use some precise methods to verify their correctness, while model checking based on time Petri nets and timed computation tree logic (TCTL) is such an effective method. However, the existing models and tools only focus on those multiprocessor real-time systems where the number of processors of the same type is just one, and thus, they cannot work for the case that the number of processors of the same type is greater than one. Hence, this article proposes prioritized time-point-interval Petri nets (PToPN) to deal with it and defines their firing rules and state graphs to represent their behaviors. A PToPN can explicitly model the preemptive scheduling of such a real-time system, and TCTL formulas specifying design requirements of the system can be verified based on its state graph. Besides, we propose TCTL with unknown time bounds, denoted as TCTLX, to compute the minimum or maximum time bound ensuring a related formula holds. Such a quantitative analysis is very necessary in the real applications because they can be used to compute some performances of a system such as the worst-case execution time of tasks and the idle time of processors. We design the related algorithms and develop a tool. We use a real example from HUAWEI Company to show the usefulness of our method, and do some experiments to show the advantages of our method compared with another state-of-the-art one.

Automated summary

When performing real-time tasks with dependent relations in a multiprocessor interruptible environment, the correct design of such a system is complex and difficult. Model checking based on time Petri nets and timed computation tree logic (TCTL) is an effective method to verify the correctness of the system. However, existing models and tools only focus on multiprocessor real-time systems with one processor of the same type, leaving out cases with more than one. This article proposes prioritized time-point-interval Petri nets (PToPN) to address this issue, with defined firing rules and state graphs to represent the system's behaviors. We also introduce TCTL with unknown time bounds (TCTLX) to compute the minimum or maximum time bounds ensuring a related formula holds.