Specification of concurrent systems using graph grammars

Abstract

Existing textual programming languages support sequential programming well because there is a correlation between the one-dimensional nature of text and the one-dimensional nature of sequential programs, i.e. the single flow of control in a program. Textual notation does not support concurrent programming as well, however, because concurrent programs have many threads of control, have a two-dimensional relationship between the flow of control in a process and the flow of information between processes, and are often dynamic. Most existing models for the specification of concurrent systems support one or two of these traits, but fall short of supporting all three.

Graph grammars are well suited for the specification of concurrent systems because they are also inherently concurrent, two-dimensional, and dynamic. We have developed a general graph rewriting model, $\Delta$-grammars, based on the theory of graph grammars. Concurrent systems are specified in A by representing the state of the system as a graph and state transitions as graph transformations. Previously, we have developed a formal semantics for $\Delta$-grammars and demonstrated its usefulness for giving a graphical semantics of existing concurrent languages, such as Actors and GARP.

This thesis shows $\Delta$'s usefulness as a specification language. It describes how specifications are modularly and systematically designed in $\Delta$. It also describes a technique for the static analysis of $\Delta$-specifications. Classes of $\Delta$-specifications that are confluent, terminating, deadlock-free, starvation-free, or efficient to execute are recognized by examining the structure of $\Delta$-productions and the way in which $\Delta$-productions interact, both with other $\Delta$-productions and with state graphs. The technique for static analysis can be used to analyze existing $\Delta$-specifications and as a guideline for the design of correct $\Delta$-specifications.

The techniques are illustrated throughout with examples and tutorial introductions to graph grammars and $\Delta$-grammars are included.