Task 7.1: Adapting existing formal techniques to a setting of incremental evolution

The main problem is that existing verification techniques are only able to verify formal properties on a model in its entirety. Assuming that we have proven that a model satisfies some desirable properties, even the smallest incremental change to this model requires us to reverify these properties for the entire model again. Because this is a very time-consuming and computationally expensive process, it does not scale up to reasonable sized software models [MS03]. Therefore, it would be much more effective to come up with an incremental model checking and model verification technique. With such an approach, the effort needed to reverify a given property would become proportional to the change made to the model. In the literature, the problem of incremental verification is hardly addressed, especially in the context of evolving software models. A notable exception is the very recent work of [TK06] who propose an incremental verification method, based on temporal logics, for checking the consistency of component composition. A related line of research is known as a compositional verification [BFG96]. Its main goal is to attack the well-known state space explosion problem by decomposing a model into smaller parts that are easier to check and to verify. It remains an open question whether and how such techniques can be applied in the context of evolving models.

wp7/t7.1/index.txt · Last modified: 2007/10/18 17:17 by pys