There are two general approaches for scheduling tasks in real-time systems: runtime and pre-runtime scheduling. However, there are several situations where the runtime approach does not find a feasible schedule even when such a schedule exists. However, finding a feasible schedule is not trivial, because this problem is NP-Hard in its general form. The proposed method finds a pre-runtime scheduling, when one exists, using state space exploration starting from a system formal model. Despite this technique being not new, at the best of our present knowledge, no one tried to use it for finding pre-runtime scheduling. The main problem with this approach is the space size, which can grow exponentially. This paper shows how to minimize this problem. Additionally, the proposed algorithm is a depth-first search method on a labeled transition system derived from a time Petri net model. It is verified through real-world experimental results that the schedule is found examining a reduced number of states.