False positives during model checking

[alex.t...@gmail.com]

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.

[Stephan Merz]

Unlike static analysis, standard model checkers such as TLC do not apply abstractions to the input model, and in this sense they do not produce false positives. However, the specification given to the model checker is always an abstraction of the real system and therefore counter-examples found by the model checker need not correspond to actual system executions. In those cases, either the property must be reformulated or the model must be refined to exclude such spurious counter-examples, and the latter may lead to state explosion and may render verification infeasible.

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5985a9d4-fa8f-47e2-90a5-fa75cde9a736n%40googlegroups.com.

[alex.t...@gmail.com]

Thanks a lot Stephan for your reaction as usual ).
Yes. Two solutions you offered are quite obvious. But the problem is i cant accept them ). If i change the property we are at risk of omitting false negatives which is unacceptable, in case of model refinement as you said we get state explosion.
So i thought may be there is a concept of using something like ignore state variables... in a similar way we use prophecy variables, history or stuttering variable. Say, first we determine the source of imprecision (concrete action) with an error stack trace. Then we associate that action with the problematic action which causes the fp invariant check violation using that ignore variable, we check the safety property iff there is no association between the source of imprecision and the last action performed...

воскресенье, 18 апреля 2021 г. в 12:31:12 UTC+3, Stephan Merz: