[SAL-HELP] Question about k-induction and real-time systems verification

[Zonghua Gu]

We are trying to use SAL inf-bmc with k-induction to model and check
schedulability of a set of real-time tasks by building a model of the
taskset with SAL, and checking the invariant property "the state where a
deadline is violated is unreachable". If this property holds, then the
system is schedulable, and vice versa. The problem is, we don't know how to
choose k. If we happen to find a k to prove the invariant to be true, then
we have proven that the system is schedulable; but if we have tried k =
1,2,3...100 and still cannot prove the invariant, it is always possible that
the invariant can be proven when k = 101, so we can never say for sure that
the system is not schedulable. I think this is a problem with k-induction in
general: you never know if the reason that you fail to prove a given
invariant is because k is too small, or because the invariant is false.
Even if you have tried k = 1 up to 10000 and found the invariant false, you
still cannot say for sure that it is false.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.csl.sri.com/pipermail/sal-help/attachments/20080630/50689652/attachment.html