Wenzel, SvenSvenWenzelWarzecha, DanielDanielWarzechaJürjens, JanJanJürjensOchoa, MartinMartinOchoaPoggenpohl, DanielDanielPoggenpohl2022-03-042022-03-042014https://publica.fraunhofer.de/handle/publica/23543910.1016/j.csi.2013.12.011In model-based development, quality properties such as consistency of security requirements are often verified prior to code generation. Changed models have to be re-verified before re-generation. If several alternative evolutions of a model are possible, each alternative has to be modeled and verified to find the best model for further development. We present a verification strategy to analyze whether evolution preserves given security properties. The UMLchange profile is used for specifying potential evolutions of a given model simultaneously. We present a tool that reads these annotations and computes a delta containing all possible evolution paths. The paths can be verified wrt. security properties, and for each successfully verified path a new model version is generated automatically.enmodel evolutionsecurity verificationUML profiletool support400journal article