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

For decades, schedulability analysis of Cyber-Physical Systems (CPS) has been conducted by analytical methods rather than model-based methods. However, CPS are getting more and more complicated, beyond the capability of analytical methods, as more sophisticated scheduling mechanisms are used. This encourages the use of model-based and automated verification techniques. These techniques must be flexible enough to be adapted to any system, and easy to use by system designers, without deep knowledge of formal verification. In this paper, we present a flexible model-based framework for specifying hierarchical scheduling systems and performing automated formal verification. It allows to easily specify complex scheduling mechanisms, with hierarchical scheduling units that can be analyzed efficiently in a compositional manner. Formal verification using statistical techniques is performed automatically by generating on-the-fly the formal models. Finally, the framework returns comprehensible feedback from the results of formal verification in the design tool.