Specifying concurrent systems with Δ-grammars

A graph-grammar-based notation for specifying concurrent and distributed systems is introduced. The notation has a formal algebraic basis that both defines the meanings of graphs and forms the foundation for verifying transformations from specifications to code. Specifications show no implementation bias and are therefore independent of many low-level issues that clutter up conventional notations. The use of graphics greatly simplifies the tasks of writing and understanding specifications of concurrent systems. The use of the approach is illustrated with two examples: the dynamic dining philosophers problem and the problem of establishing connections between clients in a multiple-server network with arbitrary topology in which the clients could be associated with any server.