Formal Specification and Verification of the Real-time Scheduler in FIP