Abstract
This paper describes the application of the Real-Time Maude tool to the formal specification and analysis of the CASH scheduling algorithm and its suggested modifications. The CASH algorithm is a sophisticated state-of-the-art scheduling algorithm with advanced capacity sharing features for reusing unused execution budgets. Because the number of elements in the queue of unused resources can grow beyond any bound, the CASH algorithm poses challenges to its formal specification and analysis. Real-Time Maude extends the rewriting logic tool Maude to support formal specification and analysis of object-based real-time systems. It emphasizes generality of specification and supports a spectrum of analysis methods, including symbolic simulation and (unbounded and time-bounded) reachability analysis and LTL model checking. We show how we have used Real-Time Maude to experiment with different design modifications of the CASH algorithm using both Monte Carlo simulation and reachability analysis. We could quickly and easily specify and analyze these modifications using Real-Time Maude, and discovered subtle behaviors in the modifications that lead to missed deadlines.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, Springer, Heidelberg (2004)
Buttazzo, G., Lipari, G., Abeni, L., Caccamo, M.: Soft Real-Time Systems: Predictability vs. Efficiency. Springer, Heidelberg (2005)
Caccamo, M., Buttazzo, G., Sha, L.: Capacity sharing for overrun control. In: Proc. IEEE Real-Time Systems Symposium, Orlando (December 2000)
Clavel, M., Durán, F., Eker, S., Lincoln, P., MartÃ-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and programming in rewriting logic. Theoretical Computer Science 285, 187–243 (2002)
Clavel, M., Dúran, F., Eker, S., Lincoln, P., MartÃ-Oliet, N., Meseguer, J., Talcott, C.: Maude Manual (Version 2.2) (December 2005), http://maude.cs.uiuc.edu
Gai, P., Abeni, L., Giorgi, M., Buttazzo, G.: A new kernel approach for modular real-time systems development. In: ECRTS 2001, IEEE, Los Alamitos (2001)
Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HyTech: A model checker for hybrid systems. Software Tools for Technology Transfer 1, 110–122 (1997)
Knuth, D.E.: The Art of Computer Programming: Seminumerical Algorithms, 2nd edn., vol. 2. Addison-Wesley, Reading (1981)
Lien, E.: Formal modelling and analysis of the NORM multicast protocol using Real-Time Maude. Master’s thesis, Dept. of Linguistics, University of Oslo (2004)
Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, Springer, Heidelberg (1998)
Ölveczky, P.C.: Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude (extended version), http://www.ifi.uio.no/RealTimeMaude/CASH
Ölveczky, P.C., Keaton, M., Meseguer, J., Talcott, C., Zabele, S.: Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude. In: Hussmann, H. (ed.) ETAPS 2001 and FASE 2001. LNCS, vol. 2029, Springer, Heidelberg (2001)
Ölveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Theoretical Computer Science 285, 359–405 (2002)
Ölveczky, P.C., Meseguer, J.: Specification and analysis of real-time systems using Real-Time Maude. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol. 2984, Springer, Heidelberg (2004)
Ölveczky, P.C., Meseguer, J.: Real-Time Maude 2.1. Electronic Notes in Theoretical Computer Science 117, 285–314 (2005)
Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation (to appear, 2006)
Ölveczky, P.C., Meseguer, J., Talcott, C.L.: Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude (2004), http://www.ifi.uio.no/RealTimeMaude
Thorvaldsen, S., Ölveczky, P.C.: Formal modeling and analysis of the OGDC wireless sensor network algorithm in Real-Time Maude. Manuscript (October 2005), http://www.ifi.uio.no/RealTimeMaude/OGDC
Yovine, S.: Kronos: A verification tool for real-time systems. Software Tools for Technology Transfer 1(1–2), 123–133 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ölveczky, P.C., Caccamo, M. (2006). Formal Simulation and Analysis of the CASH Scheduling Algorithm in Real-Time Maude. In: Baresi, L., Heckel, R. (eds) Fundamental Approaches to Software Engineering. FASE 2006. Lecture Notes in Computer Science, vol 3922. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11693017_26
Download citation
DOI: https://doi.org/10.1007/11693017_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33093-6
Online ISBN: 978-3-540-33094-3
eBook Packages: Computer ScienceComputer Science (R0)