Gesellschaft für Informatik e.V.

Lecture Notes in Informatics

Software Engineering 2010 P-159, 153-164 (2010).

Gesellschaft für Informatik, Bonn

Copyright © Gesellschaft für Informatik, Bonn


Modeling and verifying dynamic communication structures based on graph transformations

Stefan Henkler , Martin Hirsch , Claudia Priesterjahn and Wilhelm Schäfer


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.

Full Text: PDF

Gesellschaft für Informatik, Bonn
ISBN 978-3-88579-253-6

Last changed 04.10.2013 18:29:49