platforms with an arbitrary allocation of tasks among processors, this problem is NP-hard for most schedulers [4]. At the same time, there are polynomial algorithms for the narrow classes of systems [3]. Therefore, various algorithms [5; 6; 7; 8] are developed to test the sufficient conditions for the schedulability of systems, which evaluate real-time systems pessimistically: if the conditions are met, the system is considered to have passed the test, otherwise, its schedulability cannot be estimated. In [9], it is shown that often, with such an approach, a significant number of schedulable systems, up to 50%, can be rejected as probably non-schedulable. Similar results are shown by experiments in which sufficient tests are compared with each other [6; 7; 8]. Therefore, the development and improvement of exact methods remains a relevant task for various types of systems with different scheduling methods [9; 10; 11; 12; 13; 14]. In addition to the development of specialized methods for exact schedulability testing, there are a number of works that use general formal methods from programs and systems analysis [15]. General formal methods can provide models, algorithms, and capabilities for the exact solution of the main problem of real-time system schedulability, which are not presented in specialized approaches. For example, [PERSON]. [16; 17] study a fixed-priority scheduler representation for a multiprocessor system and systems of non-preemptive self-suspending tasks using timed automata. The paper [18] models a special case of the system in the Promela language [19] of the SPIN verifier [20], and the paper [21] presents a Promela model for a single-processor system. In [22], the authors use graph games to simplify the reachability problem in the exact schedulability test. In a recent paper [14], we used the Kripke model to formalize a real-time system with an abstract scheduler. We implement this abstract formalization for the global fixed priority and the earliest-deadline priority schedulers, as well as preemptive and non-preemptive tasks, in Promela [23]. Our experiments with the model checker SPIN and Promela models for these real-time systems show that the exact schedulability test is only reliably completed for five processors and six tasks. As we increase the number of processors and tasks, the SPIN test begins ti take too long. This expected result motivates us to develop a more practical approach, as described in this paper. In this paper, we study the problem of an exact schedulability test for systems in which sporadic tasks have a global fixed priority (GFP) and are not preemptive (NP). Such systems are known to be particularly sensitive to task parameters such as their execution time and relative deadline. At the same time, the class of real-time systems in which sporadic tasks should not be preempted and have a strictly defined priority--NP-GFP systems--is quite wide. In such systems, task preemption can be expensive due to the complexity or impossibility of restoring the context of interrupted jobs or computations. This class includes, for example, systems for distributing resources (memory, physical space in a warehouse) among occasionally arriving consumers (computing processes, cargo), message transmission systems with different message importance and/or urgency, big data processing systems, the trajectory and velocity planning of emergency rescue vehicles for collision avoidance [24], critical exception processing tasks in avionics and spacecraft industry control systems, etc. There are several works on schedulability tests for variants of such systems [1; 2; 6; 7; 8; 17; 25; 26; 27; 28]. We discuss them in Section 5. We propose an approach to the schedulability test problem that uses a formal representation of real-time systems as Kripke models, which are widely used in program and system verification [29].