[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] False positives during model checking

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:


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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5985a9d4-fa8f-47e2-90a5-fa75cde9a736n%40googlegroups.com.