|
|
|
|
|
02224 Modelling and Analysis of Real-Time Systems Spring 2024 |
Modelling Scheduling in Uppal |
Although at tool like the Times Tool may be used for analyzing schedulability for processes with a standard structure, they are not powerful enough to analyze more generel process behaviours.
Whereas UPPAAL is suited for expressing complex timed behaviour, it does not take scheduling (ie. the share of resources such as cpu-time) into account. It is, however, possible to model scheduling within Uppaal itself.
Basiscally any such model must explicitly express the time consumption of process actions and a dedicated scheduler process must switch the execution among active processes according to some scheduling principle (such as Fixed Priorities). For this to work, the processes must signal their desire to use cpu-time to the scheduler and the scheduler must indicate which process may actually execute.
A problem with this approach is the notion of preemption. If an action is preempted before finishing, its time consumption must be stalled while descheduled. However, in standard Uppal clocks cannot be stalled nor memorized.
One approach is to use discrete timing. Ie. all timing periods are assumed to be integral and the cpu-time of each process is kept track of in integer variables.
An example of how such discrete scheduling can be modelled is given by the following Uppaal model
CAVEAT: The discrete schedulers shown here have an issue with strict invariants in Uppaal version 5.0 and 5.1. Alhough marked as syntax errors, Uppaal 5.x will work with them anyhow. However, you may instead download and use the older version 2.26-1 for which the verification is about 3-4 times faster.
This model includes a general scheduler which schedules a set of processes according to fixed priority scheduling. The examples desmonstrates this for a set of periodic tasks, but in general, the process can have any structure, as long as they interact with the scheduler properly (documented in the declaration part of the Scheduler component).
A special issue is that processes which have reached their maximum computation time should be considered done and not be preempted by higher priority processes which are realeased at that very moment. Therefore processes with zero remaining time are not allowed to be preempted allowing for 100 % utilization in certain cases.
On the other hand, some process actions (like simple setting of variables) may take negligible time but may still be preempted anyhow (just when they are about to be executed). For this, the scheduler provides at special timing value (DELTA) which indicates a preemptable process which takes no (significant) time. An example of this is given by the UPPAL model:
Here a process which periodically generes a pulse on an output signal may be preempted by a periodic worker task. The cpu-usage of this may cause the pulse to suffer from jitter and/or widening as expressed by the queries.
A problem with discrete modelling is that state explosion is likely to occur due to the fine granularity.
It may seem that UPPAAL with stopwatches be an an ideal solution to the preemption problem. When a process is preempted, an associated cpu-consumption clock could be stopped and started again when the process is rescheduled.
Alas, due to the impreciseness associated with stopwatches, the scheduling model may not be able to confirm scheduling which is known to be feasible. There are, however, some tweaks which may be applied to make the model more precise:
As an example, consider the model
which models fixed priority scheduling (using the process identifiers as priorities) for periodically released processes.
This model is able to confirm schedulability for the given set of scheduling parameters. Note that integral relase times is accomoplished by making the initial Process state urgent. If urgency is dropped, the verification becomes indeterminate.
For alternative modelling approaches with stopwatches see also the paper
Model-Based Framework for Schedulability Analysis Using UPPAAL 4.1