Explorations on the formal frontier of distributed system design

Abstract

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.>