Explorations on the formal frontier of distributed system design

The author explores part of the boundary of formal design, seeking to apply formal techniques to aid in the derivation of a distributed design. This is demonstrated on the rederivation of the train signaling protocol developed in the 19th century. It was this protocol that gave rise to the now-familiar concept of semaphore. However, a study of the train system shows that there is much more to its protocol than simply the instantiation of the semaphore concept. This exploration places on a more formal footing issues such as discovery of the need for information, and the origin of key invariants, without requiring that the solution be known in advance