Sciweavers

Share
FASE
2006
Springer

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

9 years 10 months ago
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. ...
Peter Csaba Ölveczky, Marco Caccamo
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where FASE
Authors Peter Csaba Ölveczky, Marco Caccamo
Comments (0)
books