Title
Analysis of Scheduling Behaviour using Generic Timed Automata
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 gerdsmeier160.86
Rachel Cardell-Oliver227133.25