The research reported here shows how to apply the ASM (Abstract State Machines) method to define and analyse algorithms with advantage at various levels of abstraction, in a rigorous but concise way.
Lamport’s Bakery Algorithm (see abstract). For a textbook presentation of this algorithm see Chapter 6.4 of the
AsmBook where also numerous other real-time distributed algorithms are presented.