The dynamicity inherent in today's software is on the one hand a key feature which allows to build robust applications in dynamically changing, distributed environments. On the other hand, it introduces new major challenges in the design and formal analysis of such software. In this thesis, we therefore study formal methods for static as well as dynamically reconfigurable component-based software. Dynamic reconfiguration has broad applications, ranging from service-oriented software to embedded systems as used, e.g., in the automotive industry.
In this thesis, we propose to use the exogenous coordination language Reo for integrating and orchestrating distributed and potentially heterogeneous software components. Based on automata and process algebra models for the semantics of Reo, we show how the methodology of model checking can be applied to verify the behavior of component connectors modeled in Reo. Specifically, we use the mCRL2 specification language and model checking tool to analyze static component connectors. This approach enables us to validate some of the advanced modeling features of Reo, including data-, context- and time-dependent behavior.
As a formal approach for modeling structural changes, i.e., reconfigurations of component connectors, we utilize the well-studied theory of algebraic graph transformation. We argue that the application of graph transformation in this field has major advantages over ad hoc reconfiguration approaches. Graph transformation can naturally express both structural and behavioral aspects of software systems. Moreover, the rule-based rewriting approach in graph transformation allows to define reconfigurations at a high level of abstraction and with an atomic execution semantics. The existence of formal analysis techniques and an extensive tool support were additional motivation for the use of graph transformation.
In this thesis, we show how to formally model and analyze dynamic reconfiguration scenarios in Reo using graph transformation. Using model checking and the so-called critical pair analysis known from rewrite systems, our reconfigurable connector models can be inspected for potentially harmful interplay of dynamic reconfigurations, on the one hand, and the execution itself, on the other. Additionally, we demonstrate how quantitative properties of reconfigurable connectors, e.g., steady state probabilities, can be analyzed in our framework as well.
To remove the limitations of centralized coordination models, we extend our reconfiguration approach to distributed connectors. For this purpose, we use the theory of distributed graph transformation. As a new general result in the field of distributed graph transformation, we show that the flattening operation for distributed graphs is compositional. We argue that this result is relevant for transparent implementations of distributed connector models.
In the last chapter of this thesis, we show how to integrate an automata-based semantic model of Reo with our graph transformation based reconfiguration approach. We argue that this is a key ingredient to analyze problems in the domain of dynamic reconfiguration, such as state transfer and state consistency. For showing that the semantics is compositional in this approach, we reuse our earlier result on compositionality of the flattening operation for distributed graphs.
To highlight the practical relevance of the methods proposed in this thesis we provide an extensive tool support. The Eclipse Coordination Tools (ECT) which have been implemented in the context of this thesis provide an integrated environment for modeling and analysis of component connectors in Reo. For the formal analysis approaches considered in this thesis we use a number of verification tools (partially as back-ends of ECT),i.e., AGG, CADP, Henshin, mCRL2 and PRISM.
Summarizing, this thesis proposes formal models, verification techniques and tools to cope with the problems arising in the area of dynamically reconfigurable component connectors.