Many real-time systems are safe-critical, so their timing correctness must be ensured under any circumstance at runtime. To guarantee this, we should describe the system behavior by some rigorous models, based on which properties of interests can be proved. Research on formal modeling and analysis of real-time systems has been done in, at least, two research areas: real-time scheduling and…