|Real-Time Maude Case Study: The CASH Scheduling Algorithm|
This page reports on the application of Real-Time Maude by Peter Ölveczky and Marco Caccamo at the University of Illinois at Urbana-Champaign to specify and analyze a sophisticated scheduling protocol with advanced capacity sharing features that had been developed by Caccamo, Buttazzo, and Sha. The reason for the analysis was that Caccamo wanted to experiment with some possible modifications of the CASH algorithm before embarking on the laborious task of proving the modifications correct and/or implementing the changed protocols on real-time kernels for testing. It is particularly interesting that the protocol needs "infinite" data types. It turns out that the number of elements in the capacity sharing queue can grom beyong any bound. Therefore, this algorithm cannot be modeled by finite-control formalisms such as timed or hybrid automata, and cannot be model checked by traditional model checking techniques.
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.
|The Executable Real-Time Maude 2.1 Specification of CASH|