| Popis: |
With the growing complexity and autonomy of software-intensive systems, abstract modeling to study and formally analyze those systems is gaining on importance. Graph rewriting is an established, theoretically founded formalism for the graphical modeling of structure and behavior of complex systems. A graph-rewriting system consists of declarative rules, providing templates for potential changes in the modeled graph structures over time. Nowadays complex software systems, often involving distributedness and, thus, concurrency and reactive behavior, pose a challenge to the hidden assumption of global knowledge behind graph-based modeling; in particular, describing their dynamics by rewriting rules often involves a need for additional control to reflect algorithmic system aspects. To that end, controlled graph rewriting has been proposed, where an external control language guides the sequence in which rules are applied. However, approaches elaborating on this idea so far either have a practical, implementational focus without elaborating on formal foundations, or a pure input-output semantics without further considering concurrent and reactive notions. In the present thesis, we propose a comprehensive theory for an operational semantics of controlled graph rewriting, based on well-established notions from the theory of process calculi. In the first part, we illustrate the aforementioned fundamental phenomena by means of a simplified model of wireless sensor networks (WSN). After recapitulating the necessary background on DPO graph rewriting, the formal framework used throughout the thesis, we present an extensive survey on the state of the art in controlled graph rewriting, along the challenges which we address in the second part where we elaborate our theoretical contributions. As a novel approach, we propose a process calculus for controlled graph rewriting, called RePro, where DPO rule applications are controlled by process terms closely resembling the process calculus CCS. In particular, we address the aforementioned challenges: (i) we propose a formally founded control language for graph rewriting with an operational semantics, (ii) explicitly addressing concurrency and reactive behavior in system modeling, (iii) allowing for a proper handling of process equivalence and action independence using process-algebraic notions. Finally, we present a novel abstract verification approach for graph rewriting based on abstract interpretation of reactive systems. To that end, we propose the so-called compasses as an abstract representation of infinite graph languages and demonstrate their use for the verification of process properties over infinite input sets. |
