Dealing with Incompleteness in Automata-Based Model Checking

A software specification is often the result of an iterative process that transforms an initial incomplete model through refinement decisions. A model is incomplete because the implementation of certain functionalities is postponed to a later development step or is delegated to third parties. An unspecified functionality may be later replaced by alternative solutions, which may be evaluated to analyze tradeoffs. Model checking has been proposed as a technique to verify that a model of the system under development is compliant with a formal specification of its requirements. However, most classical model checking approaches assume that a complete model of the system is given: they do not support incompleteness. A verification-driven design process would instead benefit from the ability to apply formal verification at any stage, hence also to incomplete models. After any change, it is desirable that only the portion affected by the change, called replacement, is analyzed. To achieve this goal, this paper extends the classical automata-based model checking procedure to deal with incompleteness. The proposed model checking approach is able not only to evaluate whether a property definitely holds, possibly holds or does not hold in an incomplete model but, when the satisfaction of the specification depends on the incomplete parts, to compute the constraints that must be satisfied by their future replacements. Constraints are properties on the unspecified components that, if satisfied by the replacement, guarantee the satisfaction of the original specification in the refined model. Each constraint is verified in isolation on the corresponding replacement.