Formal Verification Techniques in Model Evolution

This work has been finished in July 2015.

Correctness with respect to its specification is, with varying degree, crucial for all software developed today. Software that is developed following the model based development (MBD) approach is no exception to this observation. Consider a typical MBD workflow: a model is successively altered and refined up to the point when the model is transformed into executable code. Suppose an error has been introduced in the course of the various refinements. Without proper verification techniques this error can propagate through all subsequent refinements and into the executable code. Clearly, this circumstance is undesirable. In this thesis I will thus develop a model checking-based framework for the verification of MBD artifacts that (a) offers a high-degree of automation as compared to existing approaches and (b) allows the user to model the software and write the specification in the same familiy of languages, e.g., the system is modeled using UML and the specification is written in OCL.