Parameterised three-valued model checking

• We introduce parameterised three-valued model checking for abstractions with unknown parts.
• We show that the application of parameterisation can significantly enhance the precision of three-valued abstractions.
• We develop a verification framework for software systems based on CEGAR and parameterisation.
• We develop a direct algorithm for parameterised three-valued model checking.
• Our framework allows verification of properties of the form ‘always p’ and ‘always eventually p’, where p is atomic.

Three-valued abstraction is an established technique in software model checking. It proceeds by generating a 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 models. In case of an unknown result, the abstraction is iteratively refined until a definite result can be obtained. In this paper, we present and extend our work on parameterised three-valued model checking (PMC). In our parameterised three-valued 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 specific 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 unchanged along all states of a certain path’. We demonstrate that such facts can be automatically derived from the system to be verified and that covering these facts in an abstract model can be crucial for the success and the efficiency of checking temporal logic safety and liveness properties. Parameterisation enhances the precision of three-valued models without increasing their state space, but it leads to an exponential increase in time complexity, since any property of interest must be checked for each possible parameter instantiation. In this extended paper, we introduce a novel algorithm for direct parameterised three-valued model checking that straightly explores the parameterised state space and thus avoids to construct all instantiations explicitly. We present example verification tasks where the application of our direct algorithm considerably reduces the time effort of PMC.