TY - GEN
T1 - Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude
AU - Ölveczky, Peter Csaba
AU - Caccamo, Marco
PY - 2006
Y1 - 2006
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=33745784778&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33745784778&partnerID=8YFLogxK
U2 - 10.1007/11693017_26
DO - 10.1007/11693017_26
M3 - Conference contribution
AN - SCOPUS:33745784778
SN - 3540330933
SN - 9783540330936
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 357
EP - 372
BT - Fundamental Approaches to Software Engineering - 9th International Conference, FASE 2006. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Proceedings
PB - Springer
T2 - 9th International Conference on Fundamental Approaches to Software Engineering, FASE 2006. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006
Y2 - 27 March 2006 through 28 March 2006
ER -