Automating transformational design for distributed programs

We address the problem of designing concurrent, reactive, nonterminating programs. Our approach to developing concurrent programs involves the use of correctness-preserving transformations to realize each step of program development. The transformations we have designed automatically guarantee the preservation of the deadlock freedom property, and hence deadlock freedom does not have to be manually verified after each development step. Since our transformations are syntactic, they are easily mechanizable as well. This makes syntactic transformations particularly appealing for the development of large, complex, and correct distributed systems, where a manual approach would be prohibitively expensive. In this work we present a set of syntactic transformations along with an example of their application to the development of a simplified mobile telephone system