[SAL-HELP] Modeling real-time systems with SAL

[Ashish Tiwari]

Dear Zonghua,

> It is easy to model a strictly periodic task with this technique, but I
> would like to model a sporadic task with a minimum inter-arrival time of T,
> where there may be arbitrary delay D between any two consecutive invocations
> of the task as long as D >= T. If D has an upper bound, then I can also
> model it easily. But how do I model the situation where D ranges from T to
> infinity?

You can define a type such as:

GreaterThanT : TYPE = { x : NATURAL | x >= T };

and then declare

D: GreaterThanT

Since this is now an infinite-state system, you may not be able
to use all the sal tools on this new model though.

Regards,
Ashish


> -- 
> Best,
>
> Zonghua
>