Model evolution and refinement

Software changes during its lifetime. Likewise, software models change during their design time, e.g. by removing, adding or changing operations and classes. This is referred to as model evolution. In a refinement-based approach to software design, we moreover do not deal with a single but with a chain of models (viz. formal specifications), related via refinement. Changes thus need to be consistently made to all specifications in the chain so as to keep the refinement structure.In this paper, we develop co-evolutions of models in the context of the formal method Object-Z. More specifically, given a particular evolution of a specification we show how to construct a corresponding evolution for its refinements such that the refinement relationship is kept. A chain of models can thus be systematically and consistently evolved, while maintaining the given refinement structure.