Abstract
We propose a modeling framework for performing schedulability analysis by using Uppaal real-time model-checker [2]. The framework is inspired by a case study where schedulability analysis of a satellite system is performed. The framework assumes a single CPU hardware where a fixed priority preemptive scheduler is used in a combination with two resource sharing protocols and in addition voluntary task suspension is considered. The contributions include the modeling framework, its application on an industrial case study and a comparison of results with classical response time analysis.
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
Preview
Unable to display preview. Download preview PDF.
References
Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: TIMES – a tool for modelling and implementation of embedded systems. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 460–464. Springer, Heidelberg (2002)
Behrmann, G., David, A., Larsen, K.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)
Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: Uppaal-tiga: Time for playing games! In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 121–125. Springer, Heidelberg (2007)
Bøgholm, T., Kragh-Hansen, H., Olsen, P., Thomsen, B., Larsen, K.G.: Model-based schedulability analysis of safety critical hard real-time java programs. In: Bollella, G., Locke, C.D. (eds.) JTRES. ACM International Conference Proceeding Series, vol. 343, pp. 106–114. ACM, New York (2008)
Burns, A.: Preemptive priority based scheduling: An appropriate engineering approach. In: Principles of Real-Time Systems, pp. 225–248. Prentice-Hall, Englewood Cliffs (1994)
Christensen, S., Kristensen, L., Mailund, T.: A Sweep-Line method for state space exploration. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 450–464. Springer, Heidelberg (2001), http://dx.doi.org/10.1007/3-540-45319-9_31
David, A., Illum, J., Larsen, K.G., Skou, A.: Model-Based Framework for Schedulability Analysis Using UPPAAL 4.1. In: Model-Based Design for Embedded Systems, pp. 93–119. CRC Press, Boca Raton (2010)
Fersman, E.: A generic approach to schedulability analysis of real-time systems. Acta Universitatis Upsaliensis (2003)
Kristensen, L., Mailund, T.: A generalised Sweep-Line method for safety properties. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 215–229. Springer, Heidelberg (2002), http://dx.doi.org/10.1007/3-540-45614-7_31
Palm, S.: Herschel-Planck ACC ASW: sizing, timing and schedulability analysis. Tech. rep., Terma A/S (2006)
Terma A/S: Herschel-Planck ACMS ACC ASW requirements specification. Tech. rep., Terma A/S (Issue 4/0)
Terma A/S: Software timing and sizing budgets. Tech. rep., Terma A/S (Issue 9)
Waszniowski, L., Hanzálek, Z.: Formal verification of multitasking applications based on timed automata model. Real-Time Systems 38(1), 39–65 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mikučionis, M. et al. (2010). Schedulability Analysis Using Uppaal: Herschel-Planck Case Study. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification, and Validation. ISoLA 2010. Lecture Notes in Computer Science, vol 6416. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16561-0_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-16561-0_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16560-3
Online ISBN: 978-3-642-16561-0
eBook Packages: Computer ScienceComputer Science (R0)