Modular Specification and Analysis of Distributed Algorithms

Modularity is an important engineering property that specifications should have, to allow specifications to grow larger and to modularly reason about them, when possible. These aspects fall quite appropriately in the context of the specification of distributed algorithms, where envi-ronment issues should be abstracted and the specification should focus on the problem that the algorithm claims to solve. Moreover, to reuse specifications, in a semantics preserving manner, is indeed a desirable feature. This paper proposes the use of modular structural operational semantics (MSOS) as a semantic framework for such specifications and advocates the use of the Maude MSOS Tool to support the execution and analysis of the MSOS specifications of distributed algorithms.