Modeling and verifying dynamic communication structures based on graph transformations

Abstract

Current and especially future software systems increasingly exhibit socalled self* properties (e. g. , self healing or self optimization). In essence, this means that software in such systems needs to be reconfigurable at runtime to remedy a detected failure or to adjust to a changing environment. Reconfiguration includes adding or deleting software components as well as adding or deleting component interaction. As a consequence, the state space of self* systems becomes so complex, that current verification approaches like model checking or theorem proving usually do not scale. Our approach addresses this problem by first defining a so-called “regular” system architecture with clearly defined interfaces and predefined patterns of communication such that dependencies between concurrently running component interactions are minimized with respect to the system under construction. The construction of such architectures and especially its reconfiguration is controlled by using graph transformation rules which define all possible reconfigurations. It is formally proven that such a rule set cannot produce any “non-regular” architecture. Then, the verification of safety and liveness properties has to be carried out for only an initially and precisely defined set of so-called coordination patterns rather than on the whole system.