Download Assertion Language manual - Bound

Handle (Message = 31)
...
Log (Message)
Log (Msg = 31)
if Free = 1 and Msg /= Log_Full then
Handle (Log_Full);
else
...
end if;
Handle (Message = 99)
...
Log (Message)
Log (Msg = 99)
if Free = 1 and Msg /= Log_Full then
...
else
Free := Free - 1;
Buffer(Buffer’Last - Free) := Msg;
end if;
Figure 7: Longest call path in recursion example
Slicing recursive call-paths
How can we find an upper bound on the execution time of the recursive call-path in the above
example? Asking Bound-T to analyse Handle will just result in error messages that complain
about the recursion.
You can make Bound-T analyse a piece of a recursive call-path by asserting the execution time
of one of the subprograms in the call-path. The calls in this subprogram are thereby hidden
from Bound-T which breaks the recursive cycle (if there are several recursion cycles you may
have to break the other cycles in the same way). This analysis gives the WCET for the rest of
the call-path. Then you analyse the call-path again but this time you assert the execution time
of another subprogram in the call-path. You can then combine the WCET bounds on the pieces
to compute the WCET bound for the whole call-path. However, you also have to be careful to
guide Bound-T to choose the right paths within each subprogram. Below we show how to do it
for the example.
Slicing the example
For our example we can start by hiding the Log subprogram and analysing the Handle
subprogram. Since Handle always calls Log, the analysis always includes the desired path
within Handle whatever execution time we assert for Log; assume we choose 0 cycles so that
the assertions for this analysis are
subprogram "Errors.Log" time 0 cycles; end "Errors.Log";
Assume that the resulting WCET bound for Handle is 422 cycles. Since zero cycles are
assumed for Log this means that the WCET for Handle alone is 422 cycles.
74
Recursion
Bound-T Assertion Language