Specification of real-time software and verification of their schedulability using hybrid automata

摘要

Real-time software runs over real-time operating systems, and guaranteeing qualities is difficult. In this paper, we formally specify real-time software and verify its schedulability. 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.