Protocols that govern the interactions between software components are a popular means to support the construction of correct
component-based systems. Previous studies have, however, almost exclusively focused on static component systems that are not
subject to evolution. Evolution of component-based systems with explicit interaction protocols can be defined quite naturally
using aspects (in the sense of AOP) that modify component protocols. A major question then is whether aspect-based evolutions
preserve fundamental correctness properties, such as compatibility and substitutability relations between software components.
In this paper we discuss how such correctness properties can be proven in the presence of aspect languages that allow matching
of traces satisfying interaction protocols and enable limited modifications to protocols. We show how common evolutions of
distributed components can be modeled using VPA-based aspects [14] and be proven correct directly in terms of properties of
operators of the aspect language. We first present several extensions to an existing language for VPA-based aspects that facilitate
the evolution of component systems. We then discuss different proof techniques for the preservation of composition properties
of component-based systems that are subject to evolution using protocol-modifying aspects.
Work partially supported by AOSD-Europe, the European Network of Excellence in AOSD (www.aosd-europe.net).