Abstract
This paper presents a compositional approach for schedulability analysis of hierarchical systems, which enables to prove more systems schedulable by having richer and more detailed scheduling models. We use a lightweight method (statistical model checking) for design exploration, easily assuring high confidence in the correctness of the model. A satisfactory design can be proved schedulable using the computation costly method (symbolic model checking). In order to analyze a hierarchical scheduling system compositionally, we introduce the notion of a stochastic supplier modeling the supply of resources in each component. We specifically investigate two different techniques to widen the set of provably schedulable systems: (1) a new supplier model; (2) restricting the potential task offsets. We also provide a way to estimate the minimum resource supply (budget) that a component is required to provide.
The research presented in this paper has been partially supported by EU Artemis Projects CRAFTERS and MBAT.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: Times: A tool for schedulability analysis and code generation of real-time systems. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 60–72. Springer, Heidelberg (2004)
ARINC 653. Website. https://www.arinc.com/cf/store/documentlist.cfm
Åsberg, M., Nolte, T., Pettersson, P.: Prototyping and code synthesis of hierarchically scheduled systems using TIMES. J. Conver. (Consum. Electron.) 1(1), 77–86 (2010)
Behnam, M., Nolte, T., Shin, I., Åsberg, M., Bril, R.: Towards hierarchical scheduling in VxWorks. In: OSPERT 2008, pp. 63–72 (2008)
Boudjadar, A., David, A., Kim, J., Larsen, K., Nyman, U., Skou, A.: Schedulability and energy efficiency for multi-core hierarchical scheduling systems. In: Proceedings of the International Congres on Embedded Real Time Software and Systems ERTS\(^2\) (2014)
Boudjadar, A., David, A., Kim, J.H., Larsen, K.G., Mikučionis, M., Nyman, U., Skou, A.: Hierarchical scheduling framework based on compositional analysis using uppaal. In: Fiadeiro, J.L., Liu, Z., Xue, J. (eds.) FACS 2013. LNCS, vol. 8348, pp. 61–78. Springer, Heidelberg (2014)
Bulychev, P.E., David, A., Larsen, K.G., Mikucionis, M., Poulsen, D.B., Legay, A., Wang, Z.: UPPAAL-SMC: statistical model checking for priced timed automata. In: Wiklicky, H., Massink, M. (eds.) QAPL, vol. 85, pp. 1–16. Electronic Proceedings in Theoretical Computer Science (2012). doi:10.4204/EPTCS.85.1
Carnevali, L., Pinzuti, A., Vicario, E.: Compositional verification for hierarchical scheduling of real-time systems. IEEE Trans. Softw. Eng. 39(5), 638–657 (2013)
Cassez, F., Larsen, K.G.: The impressive power of stopwatches. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, p. 138. Springer, Heidelberg (2000)
David, A., Larsen, K.G., Legay, A., Mikučionis, M.: Schedulability of Herschel-Planck revisited using statistical model checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 293–307. Springer, Heidelberg (2012)
Deng, Z., Liu, J.W.S.: Scheduling real-time applications in an open environment. In: Proceedings of the 18th RTSS, pp. 308–319. Society Press (1997)
Easwaran, A., Anand, M., Lee, I.: Compositional analysis framework using EDP resource models. In: Proceedings of the 28th IEEE International Real-Time Systems Symposium, pp. 129–138 (2007)
Easwaran, A., Anand, M., Lee, I., Phan, L.T.X., Sokolsky, O.: Simulation relations, interface complexity, and resource optimality for real-time hierachical systems (2009)
Lee, J., Phan, L.T.X., Chen, S., Sokolsky, O., Lee, I.: Improving resource utilization for compositional scheduling using DPRM interfaces. SIGBED Rev. 8(1), 38–45 (2011)
Bril, R.J., Holenderski, M., Lukkien, J.J.: An efficient hierarchical scheduling framework for the automotive domain. In: Babamir, S.M. (ed.) Real-Time Systems, Architecture, Scheduling, and Application, pp. 67–94. InTech (2012)
Mok, A.K., Feng, X.A., Chen, D.: Resource partition for real-time systems. In: Proceedings of RTAS 2001, pp. 75–84. IEEE Computer Society (2001)
ORIS. Website. http://www.oris-tool.org/
Phan, L.T.X., Lee, I.: Improving schedulability of fixed-priority real-time systems using shapers. In: Proceedings of RTAS 2013, Washington, DC, USA, pp. 217–226. IEEE Computer Society (2013)
Phan, L.T.X., Lee, J., Easwaran, A., Ramaswamy, V., Chen, S., Lee, I., Sokolsky, O.: CARTS: a tool for compositional analysis of real-time systems. SIGBED Rev. 8(1), 62–63 (2011)
Shin, I., Easwaran, A., Lee, I.: Hierarchical scheduling framework for virtual clustering of multiprocessors. In: ECRTS, pp. 181–190. IEEE Computer Society (2008)
Shin, I., Lee, I.: Periodic resource model for compositional real-time guarantees. In: RTSS, pp. 2–13. IEEE Computer Society (2003)
Shin, I., Lee, I.: Compositional real-time scheduling framework with periodic model. ACM Trans. Embedded Comput. Syst. 7(3), 1–39 (2008)
Tindell, K.: Adding time-offsets to schedulability analysis. University of York, Department of Computer Science (1994)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Boudjadar, A. et al. (2015). Widening the Schedulability of Hierarchical Scheduling Systems. In: Lanese, I., Madelaine, E. (eds) Formal Aspects of Component Software. FACS 2014. Lecture Notes in Computer Science(), vol 8997. Springer, Cham. https://doi.org/10.1007/978-3-319-15317-9_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-15317-9_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-15316-2
Online ISBN: 978-3-319-15317-9
eBook Packages: Computer ScienceComputer Science (R0)