Hierarchical Scheduling Systems
We have designed with a Cinco a framework for specifying and analyzing hierarchical scheduling systems (HSSs). These sophisticated scheduling mechanisms allows to share computation resources between several heterogeneous systems with different scheduling algorithms. These new techniques encourage the use of high performance hardware and advance software architectures in cyber-physical systems.
A hierarchical scheduling system is build with a hierarchy of scheduling unit and an interface mechanism that allows to distribute resources form the upper level to the lower levels. A scheduling unit is composed of a set of real-time tasks and a scheduling algorithm. Our framework build with Cinco allows to easily specify the structure and the parameters of such system with a graphical modeling tool automatically generated by Cinco. Moreover it allows to test the schedulability of the entire system.
One particular advantage of HSSs is that they allow a compositional verification process in which individual scheduling units are analyzed independently. This facilitates the verification of complex systems. Our framework implements such a verification process using a model-based approach with formal verification and statistical model-checking. Each scheduling unit is automatically translated into a set of timed automata models in the format of the model-checker Uppaal. Uppaal is -used to perform model-checking and statistical model-checking analyses. This proves the schedulability of the system and allows to measure its performances. Finally the results of the formal analyses are displayed graphically in the tool generated by Cinco.
The specification files to generate the HSS tool are available for download. The archive file can simply be imported “as existing project into workspace” (via File/Import/General) in Cinco version 0.6.
Uppaal 4.1.19 is needed to run formal verification on the models. It is available at the Uppaal website.
For questions regarding the HSS tool and project, please contact Louis-Marie Traonouez.
