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.
Behrmann, G., David, A., Larsen, K.G., Håkansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: QEST, pp. 125–126 (2006)
Boudjadar Abdeldjalil, David Alexandre, Kim Jin Hyun, Larsen Kim. G., Mikučionis Marius, Nyman Ulrik, Skou Arne, Hierarchical Scheduling Framework Based on Compositional Analysis Using Uppaal, Formal Aspects of Component Software (2014) ISBN:9783319076010 p.61-78, 10.1007/978-3-319-07602-7_6
Boudjadar Abdeldjalil, David Alexandre, Kim Jin Hyun, Larsen Kim Guldstrand, Mikučionis Marius, Nyman Ulrik, Skou Arne, Widening the Schedulability of Hierarchical Scheduling Systems, Formal Aspects of Component Software (2015) ISBN:9783319153162 p.209-227, 10.1007/978-3-319-15317-9_14
Bulychev Peter, David Alexandre, Larsen Kim Gulstrand, Mikučionis Marius, Bøgsted Poulsen Danny, Legay Axel, Wang Zheng, UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata, 10.4204/eptcs.85.1
Cassez Franck, Larsen Kim, The Impressive Power of Stopwatches, CONCUR 2000 — Concurrency Theory (2000) ISBN:9783540678977 p.138-152, 10.1007/3-540-44618-4_12
David Alexandre, Larsen Kim G., Legay Axel, Mikučionis Marius, Poulsen Danny Bøgsted, van Vliet Jonas, Wang Zheng, Statistical Model Checking for Networks of Priced Timed Automata, Lecture Notes in Computer Science (2011) ISBN:9783642243097 p.80-96, 10.1007/978-3-642-24310-3_7
Naujokat, S., Lybecait, M., Kopetzki, D., Steffen, B.: CINCO: A Simplicity-Driven Approach to Full Generation of Domain-Specific Graphical Modeling Tools (2016, to appear)
Phan Linh T. X., Lee Jaewoo, Easwaran Arvind, Ramaswamy Vinay, Chen Sanjian, Lee Insup, Sokolsky Oleg, CARTS : a tool for compositional analysis of real-time systems, 10.1145/1967021.1967029
Shin, I., Lee, I.: Periodic resource model for compositional real-time guarantees. In: RTSS, pp. 2–13. IEEE Computer Society (2003)
Shin Insik, Lee Insup, Compositional real-time scheduling framework with periodic model, 10.1145/1347375.1347383
Bibliographic reference
Chadli, Mounir ; Kim Jin, Hyun ; Legay, Axel ; Traonouez, Louis-Marie ; Naujokat, Stefan ; et. al. A Model-Based Framework for the Specification and Analysis of Hierarchical Scheduling Systems.FMICS-AVoCS (du 26/09/2016 au 28/09/2016). In: Lecture Notes in Computer Science Critical Systems: Formal Methods and Automated Verification, Springer International Publishing : Cham2016