Modelling and Schedulability Test of Real-Time Tasks with Timed Automata

摘要

Scheduling real-time systems with hard aperiodic tasks is often problematic. Classical approach treating a hard aperiodic task as a periodic task may be far too pessimistic and lead to very low CPU utilization. On the other hand, a hard aperiodic task is often event-driven, making it difficult to find a proper period for the task. This paper uses timed automata to model real-time tasks and the scheduler, and transforms the schedulability problem into a reachability problem. The reachability property is verified using the model checking tool Uppaal. This approach, allows us to verify other system properties while verifying the schedulability.