Formal Simulation and Analysis of the CASH Scheduling Algorithm in Real-Time Maude

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. ...

• Type: Conference
• Year: 2006
• Where: FASE
• Authors: Peter Csaba Ölveczky, Marco Caccamo
• Keywords: CASH Algorithm, FASE 2006, Formal Specification, Real-Time Maude, Software Engineering