# Converting an Arrival Curve + Worst-Case/Best-Case to a Request-Bound Function (RBF)

In the following, we show a way to convert a given arrival curve, paired with a worst-case/best-case execution time, to a request-bound function. Definitions and proofs will handle both lower-bounding and upper-bounding arrival curves.
Consider any type of tasks with a given cost ...

... and any type of jobs associated with these tasks.

Let MaxArr and MinArr represent two arrivals curves. MaxArr upper-bounds the possible number or arrivals for a given task, whereas MinArr lower-bounds it.

We define the conversion to a request-bound function as the product of the task cost and the number of arrivals during Δ. In the upper-bounding case, the cost of a task will represent the WCET of its jobs. Symmetrically, in the lower-bounding case, the cost of a task will represent the BCET of its jobs.
Finally, we show that the newly defined functions are indeed request-bound functions.

In the following section, we prove that the transformation yields a request-bound function that conserves correctness properties in both the upper-bounding and lower-bounding cases.
Section Facts.

First, we establish the validity of the transformation for a single, given task.

Consider an arbitrary task tsk ...

... and any job arrival sequence.
Variable arr_seq : arrival_sequence Job.

First, note that any valid upper-bounding arrival curve, after being converted, is a valid request-bound function.
The same idea can be applied in the lower-bounding case.
Next, we prove that the task respects the request-bound function in the upper-bounding case. Note that, for this to work, we assume that the cost of tasks upper-bounds the cost of the jobs belonging to them (i.e., the task cost is the worst-case).
Finally, we prove that the task respects the request-bound function also in the lower-bounding case. This time, we assume that the cost of tasks lower-bounds the cost of the jobs belonging to them. (i.e., the task cost is the best-case).
Next, we lift the results to the previous section to an arbitrary task set.

Let ts be an arbitrary task set...

... and consider any job arrival sequence.
Variable arr_seq : arrival_sequence Job.

First, we generalize the validity of the transformation to a task set both in the upper-bounding case ...
... and in the lower-bounding case.
Second, we show that a task set that respects a given arrival curve also respects the produced request-bound function, lifting the result obtained in the single-task case. The result is valid in the upper-bounding case...
...as well as in the lower-bounding case.
We add the lemmas into the "Hint Database" basic_rt_facts so that they become available for proof automation.
Global Hint Resolve
valid_arrival_curve_to_max_rbf
respects_arrival_curve_to_max_rbf