Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude

Peter Csaba Ölveczky; Marco Caccamo

doi:10.1007/11693017_26

Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude

Peter Csaba Ölveczky, Marco Caccamo

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

39 Scopus citations

Abstract

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.

Original language	English
Title of host publication	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
Publisher	Springer Verlag
Pages	357-372
Number of pages	16
ISBN (Print)	3540330933, 9783540330936
DOIs	https://doi.org/10.1007/11693017_26
State	Published - 2006
Externally published	Yes
Event	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 - Vienna, Austria Duration: 27 Mar 2006 → 28 Mar 2006

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	3922 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	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
Country/Territory	Austria
City	Vienna
Period	27/03/06 → 28/03/06

Access to Document

10.1007/11693017_26

Cite this

Ölveczky, P. C., & Caccamo, M. (2006). Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude. In 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 (pp. 357-372). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3922 LNCS). Springer Verlag. https://doi.org/10.1007/11693017_26

Ölveczky, Peter Csaba ; Caccamo, Marco. / Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude. 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. Springer Verlag, 2006. pp. 357-372 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{b309e71327324557a5b6afd0b5e7a811,

title = "Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude",

abstract = "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.",

author = "{\"O}lveczky, {Peter Csaba} and Marco Caccamo",

year = "2006",

doi = "10.1007/11693017_26",

language = "English",

isbn = "3540330933",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "357--372",

booktitle = "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",

note = "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 ; Conference date: 27-03-2006 Through 28-03-2006",

}

Ölveczky, PC & Caccamo, M 2006, Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude. in 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 3922 LNCS, Springer Verlag, pp. 357-372, 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, Vienna, Austria, 27/03/06. https://doi.org/10.1007/11693017_26

Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude. / Ölveczky, Peter Csaba; Caccamo, Marco.
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. Springer Verlag, 2006. p. 357-372 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3922 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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

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 Verlag

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 -

Ölveczky PC, Caccamo M. Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude. In 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. Springer Verlag. 2006. p. 357-372. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/11693017_26

Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this