B constrained

Abstract

In a previous work, we applied constraint solving techniques to problems like invariant preservation and deadlock freedom checking. The idea behind constraint based deadlock checking is that we set up a logical formula encoding a state where the invariant holds, but all guards are false. We then use the built-in constraint solver to check if the formula has a model. If we can find such a model, we know that the system cannot be proven to be deadlock free. The invariant preservation checking is similar. We encode a state where the invariant holds and a successor state (for some event) where the invariant is false. If this formula has a model, we know that the system cannot be proven correctly. Note that in both cases we do not require that the states are reachable. The system might behave correctly, but the invariant is too weak to prove its correctness.