Formalizing hierarchical scheduling for refinement of real-time systems.

•Formal definition of parameterized timing properties with proofs.•Refinement pattern to generate invariants to replace parameterized timing properties.•Refine hierarchical scheduling system with compatible scheduling policies.•Distinguish timing properties from the perspective of different system design phases.