Hello all.
I would like to ask if some one has an experience dealing with false positives during model checking (analogous to fp in static analisys)? May be i am conceptually wrong. But it seems quit obvious. FP may arirse due to some imprecision caused by abstraction. Say i want to verify information flows in some system (high inputs cant flow into low sinks). Now i have an ASSIGN statement of the form:
record1.f1 := high;
where record is an inner variable whose security label may be changed at runtime.
To simplify the model we assign label "high" to the entire record1 rather than assigning it to its field f1. This the source of imprecision.
At the next step we output the value of record1 to "low" sink as follows:
output1:=record1.f2;
and get Invariant violation which is false positive. In static analysis we simply mark such warnings as FP to ignore them in further checks.
Is there some common approach (strategy) for excluding invariant checks in some states of a model?
Thanks in advance. Alex.
--