Automating the refinement of specifications for distributed systems via syntactic transformations

The idea of successively refining an abstract specification until it contains enough detail to suggest an implementation has been investigated by numerous researchers. The emphasis to date has been on techniques that, unfortunately, lead to a large amount of manual formal labour for each refinement step. With such techniques, both the cost and the possibility of errors arising informal manipulation are high. Using a theorem prover can reduce the number of manipulation errors, but, given current technology, the amount of labour is still daunting. This research explores an alternative solution to the refinement problem, namely the use of syntactic transformations to realize each refinement step. We reduce formal labour by employing automatic transformations that guarantee the preservation of desirable properties—e.g., deadlock-freedom. Automatic transformations are particularly appealing for the development of large, complex distributed systems, where a manual approach to refinement would be prohibitively expensive. Distributed computations are, by nature, reactive and concurrent, so their correctness cannot be specified as a simple functional relationship between inputs and outputs. Instead, specifications must describe the time-varying behaviour of the system. Further difficulty is caused by the fact that such important characteristics of distributed systems as deadlock-freedom are global properties that cannot be achieved through considering local structures only. Transformations generally must encompass the entire system. This paper presents two syntactic transformations—the left-sequence introduction and the right-sequence introduction—and demonstrates that they preserve deadlock-freedom.