Synchronous distributed algoriths : a proof system
Résumé
Simulating synchronism on asynchronous networks allows to design synchronous distributed algorithms. This design relies upon a language with a clear operationnal semantic and an assertional proof system, consistent and complete. As an illustration, a synchronous election algorithm on an arbitrary topology network is formally derived and proved.