Formal Verification of Partitioned Scheduling in Real-Time Operating Systems Using Timed Automata

Partition scheduling plays a crucial role in ensuring temporal determinism and fault isolation in real-time operating systems. However, its correctness is difficult to guarantee through traditional testing due to the complexity of timing interactions and the need for exhaustive state exploration. Therefore, a rigorous and systematic verification approach is essential to ensure system design correctness under all execution scenarios.This paper presents a formal modeling and verification methodology for partition scheduling in operating systems, based on timed automata. The proposed model is developed and systematically verified using UPPAAL. It comprises four key components–Partition, Scheduler, TimeSynchronizer, and ErrorHandler–which collectively capture task execution flows, scheduling policies, clock synchronization, and fault-handling mechanisms. A comprehensive set of verification properties is defined using Linear Temporal Logic (LTL) to formally specify the system's temporal behaviors and safety requirements. The verification results confirm that the proposed approach effectively verifies partition switching correctness, time consistency enforcement, and exception recovery. This method provides a rigorous and practical formal foundation for modeling and analyzing real-time scheduling systems.