A Model-Based Framework for the Specification and Analysis of Hierarchical Scheduling Systems