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.StephanOn 18 Apr 2021, at 08:45, alex.t...@gmail.com <alex.t...@xxxxxxxxx> wrote: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.
--
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...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5985a9d4-fa8f-47e2-90a5-fa75cde9a736n%40googlegroups.com.