The study of distributed system design has tended to divide into two camps: either very formal methods that apply to severe abstractions of problems, or human-intuition-based methods that aid in forming the overall nature of a system design, but are often disconnected from the application of formal methods except as post-hoc verifications. Herein 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 there derivation of the train signalling 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.
Explorations on the formal frontier of distributed system design
Untersuchungen an der formalen Grenze des verteilten Systementwurfs
1992
9 Seiten, 1 Bild, 15 Quellen
Conference paper
English
Aerobot Design for Planetary Explorations
AIAA | 2016
|Distributed Air-Traffic Control. II: Explorations in Test Bed
British Library Online Contents | 1993
|Distributed Air-Traffic Control. II: Explorations in Test Bed.
Online Contents | 1993
|