Modeling and Verifying Dynamic Communication Structures based on Graph Transformations.
Stefan Henkler, M. Hirsch, Claudia Priesterjahn, Wilhelm Schäfer · 2010
Abstract: Current and especially future software systems increasingly exhibit so-called 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 de-tected 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 min-imized with respect to the system under construction. The construction of such archi-tectures 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. 1