Incremental verification of software models

A fundamental property of any structural software model is strong satisfiability: a lack of contradictions in the diagram allowing us to construct a finite instance with a non-empty population for each class and association that satisfies all the constraints, e.g. inheritance relationships and multiplicities of associations. For instance, if we focus on UML models annotated with OCL constraints, we want to make sure that we can instantiate the classes of the UML diagram in a way that all graphical and OCL constraints evaluate to true. Otherwise, the model is useless.

The problem is that checking satisfiability is computationally expensive, and it becomes undecidable if the model is annotated with complex integrity constraints written in an expressive language like OCL. Even worse, a problem of model verification tools for satisfiability (including our own EMFtoCSP) is that they do not support incremental verification, i.e. the ability to re-use results from previous verifications to facilitate the analysis of similar models. In short, if the model was correct before the latest modification and we know the change that has been done, is there a way to reevaluate the satisfiability by “only” looking at the modification (or the smallest possible subset of the model affected by it). As current tools are unable to do this,  time-consuming verification runs are repeated after each model change, a problem that impairs its practical application in an industrial setting.

We have now developed new techniques for the incremental verification of satisfiability in UML/OCL class diagrams. These techniques combine known methods for speeding verification, such as model slicing, with a novel approach: the use of instances of the model as certificates of satisfiability. Whenever a model is checked for satisfiability, a valid instance of the model is provided as an output of the model finder. After an update in the model, rather than re-verifying the model it may be sufficient to adjust the original valid instance as an instance of the new model to certificate that the model is still satisfiable. Note that this challenge is similar (but not the same) as the problem of incremental integrity checking where we wanted to efficiently check that the data in the system was consistent with the model constraints, not that the constraints were not contradictory among themselves.

For instance, if a new OCL invariant is added to the model, it is sufficient to check if our certificate satisfies the new invariant: if it does, our old certificate is still valid. Checking an OCL invariant on a given instance is orders of magnitude faster than invoking a model finder. Moreover, if the certificate is not valid and a model finder needs to be invoked, it may be possible to limit the verification to a subset (a slice) of the original model.

Sounds exciting? You can read all the technical details in this paper published in the JOT journal. And don’t worry, it is open access!.

As future work, we want to advance in the implementation of the method and explore effective strategies for the management of certificates. So far, our discussion of the method has assumed that we only maintain a single certificate at all times. However, it might be more efficient to maintain several certificates. These certificates could be computed offline, when the designer is performing other tasks. Then, when a resolvable change is applied, we can try to repair each of them separately. In this way, the likelihood that at least one of the available certificates can be repaired is increased. Moreover, while we have focused on UML class diagrams, most of the components of our proposal could be easily generalizable to other types of structural models and UML-like domain-specific languages. We plan to develop such adaptations to broaden the scope of our approach.