Abstract | ||
---|---|---|
A method for dynamic, automated analysis of the behaviour of real-time programs under different scheduling algorithms is presented. Each scheduling algorithm is defined by a generic timed automaton which can be instantiated with data for a particular set of tasks. The resulting network of instantiated timed automata can be analysed automatically in the model-checker Uppaal, to ensure correctness properties are satisfied. Various scheduling metrics can also be calculated. We assume that data such as worst case execution times, periods, deadlines and priorities have been pre-calculated for each task. In this paper we present generic specifications for uniprocessor scheduling using the immediate ceiling priority protocol (ICPP) and the earliest-deadline-first (EDF) algorithm and analyse the behaviour of a mine pump controller implemented in Ada95 under each scheduling algorithm. |
Year | DOI | Venue |
---|---|---|
2001 | 10.1016/S1571-0661(04)80883-1 | Electronic Notes in Theoretical Computer Science |
Keywords | Field | DocType |
earliest deadline first,satisfiability,generation time,worst case execution time,scheduling algorithm,real time | Fair-share scheduling,Computer science,Deadline-monotonic scheduling,Two-level scheduling,Theoretical computer science,Timed automaton,Rate-monotonic scheduling,Dynamic priority scheduling,Earliest deadline first scheduling,Round-robin scheduling,Distributed computing | Journal |
Volume | ISSN | Citations |
42 | 1571-0661 | 5 |
PageRank | References | Authors |
0.47 | 4 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
thorsten gerdsmeier | 1 | 6 | 0.86 |
Rachel Cardell-Oliver | 2 | 271 | 33.25 |