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.

Related Papers

1. Formal Simulation and Analysis of the CASH Scheduling Algorithm in Real-Time Maude.
   By Peter Ölveczky and Marco Caccamo.
   In L. Baresi and R. Heckel (Eds.), Fundamental Approaches to Software Engineering 2006 (FASE '06), volume 3922 of Springer Lecture Notes in Computer Science, pp. 357-372, 2006.
   This is the conference version of the report below.
2. Formal Simulation and Analysis of the CASH Scheduling Algorithm in Real-Time Maude (Extended Version).
   By Peter Ölveczky and Marco Caccamo.
   This is an extensive report on the Real-Time Maude 2.1 specification and analysis of the CASH algorithm. Its appendices give the full specification and analysis commands of the different versions of the CASH algorithm, both for Monte Carlo simulation and reachability analysis.
3. Capacity Sharing for Overrun Control.
   By Marco Caccamo, Giorgio Buttazzo, and Lui Sha.
   Proceedings of the IEEE Real-Time Systems Symposium, Orlando, Florida, December 2000.
   Describes the CASH algorithm.

The Executable Real-Time Maude 2.1 Specification of CASH

• The Real-Time Maude file: cash.rtmaude
• The real-Time Maude specification and analysis commands file for the Monte Carlo simulation version: cash-sim.rtmaude.
• How to execute/analyze these specifications?
  1. Start Real-Time Maude 2.1.
  2. Load the above file cash.rtmaude.
  3. To execute the CASH specification, you can start Maude with the file cash.rtmaude as argument: The various analysis commands are in this file, but are commented away; just remove the '***' parts around the commands, or cut-and-paste the desired command onto the Maude command line.