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.