Deductive schedulability verification methodology of real-time software using both refinement verification and hybrid automata

Real-time software runs over real-time operating systems, and guaranteeing qualities is difficult. As timing constraints and resource allocations are strict, it is necessary to verify schedulability, safety and liveness properties. In this paper, we formally specify real-time software using hybrid automata and verify its schedulability using both deductive refinement theory and scheduling theory. In this case, the above real-time software consists of periodic processes and a fixed-priority preemptive scheduling policy on one CPU. Using our proposed methods, we can uniformally and easily specify real-time software and verify its schedulability based on hybrid automata. Moreover, we can verify its schedulability at design stage.