Towards correct evolution of components using VPA-based aspects

Abstract. Interaction protocols are a popular means to construct correct component-based systems. Aspects that modify such protocols are interesting in this context because they support the evolution of such components. A major question then is whether aspect-based evolutions preserve fundamental notions of correctness, in particular compatibility and substitutability, of components. In this paper we discuss how such component correctness properties can be proven in the presence of aspect languages of limited expressiveness. Concretely, we show how common evolutions involving VPA-based aspects [12] can be proven correct directly in terms of operators of the aspect language. Furthermore, we present first ideas of how to use existing model checkers for the automatic verification of such properties. 1 Motivation Interaction protocols are a popular means to construct correct component-based systems and document them [19, 6]. Relying on explicit protocols, evolution of component-based sys...

• Type: Conference
• Year: 2007
• Where: ECOOP
• Authors: Dong Ha Nguyen, Mario Südholt
• Keywords: Component-based Systems, Correct Component-based Systems, ECOOP 2007, Interaction Protocols, Programming Languages