Modelling Concurrency by Tabular Expression

Yuwen Yang


Tabular expressions (Parnas et al) [26,27,29,31,32] are a software specification technique that becomes increasingly popular in software industry. The current state of the technique is restricted to sequential systems only. In this thesis we show how concurrency can be treated in some systematic way in the framework of tabular expressions.

A precise notion of composite global automata (compare [20,36])will be defined. The tabular expressions [24,26,28] used by Software Engineering Research Group will be slightly extended to deal with the transition function/relation of concurrent automata.

In the thesis, each sequential process is viewed as a Finitely Defined Automaton with Interpreted States [18], and all of the processes in the system are composed to a global finite state automata to model the concurrent system. The thesis starts with a common model of a nondeterministic finite automaton, extends the traditional automata, and associates two sets called synchronization set and competition set, respectively, to each action of the individual processes. Finally, whole processes in the system are composed and the actions dependence of individual process is eliminated for the global action. A simple example of Readers-Writers is given to illustrate this method.