Towards a derivational style of distributed system design — An example

摘要

Rederivation of the train signalling protocol developed in the 19th century is used to illustrate the application of several formal techniques to assist in the derivation of an implementation of a simple distributed system from its specification. It was this train signalling protocol that gave rise to the now-familiar concept ofsemaphore. However, a study of the train system shows that there is much more to its protocol than simply the instantiation of the semaphore concept.