Abstract:
Three-valued abstraction is an established technique in software model checking. It proceeds by generating an abstract state space model over the values true, false and unknown, where the latter value is used to represent the loss of information due to abstraction. Temporal logic properties can then be evaluated on such three-valued models. In case of an unknown result, the abstraction is iteratively refined, until a level of abstraction is reached where the property of interest can be either proven or refuted. In this paper, we introduce parameterised three-valued model checking. In our new type of abstract models, unknown parts can be either associated with the constant value unknown or with expressions over boolean parameters. Our parameterisation is an alternative way to state that the truth value of certain predicates or transitions is actually not known and that the checked property has to yield the same result under each possible parameter instantiation. A novel feature of our approach is that it allows for establishing logical connections between parameters: While unknown parts in pure three-valued models are never related to each other, our parameterisation approach enables to represent facts like 'a certain pair of transitions has unknown but complementary truth values', or 'the value of a predicate is unknown but remains constant along all states of a certain execution path'. We demonstrate that such facts can be automatically derived from the software system to be verified and that covering these facts in an abstract model can be crucial for the success and efficiency of checking temporal logic properties. Moreover, we introduce a fully automatic software verification framework based on counterexample-guided abstraction refinement and parameterisation.
