Towards Formal Verification of Distributed Algorithms

Model checking is an automatic verification technique, which provides an answer to the question whether a program, given as a state-transition system, satisfies its specification, given in terms of a temporal-logic formula. Model checking is very well studied as far as boolean finite-state programs are concerned [CGP99]. To take into account several sources of infinity such as an unknown number of processes or infinite data structures, the classical setting has been extended in several orthogonal directions. In the context of concurrent programs, one may ask whether a specification is satisfied independently of the number of participating processes. This question is referred to as parameterized verification (see [Esp14] for an overview). Second, a system may have to cope with variables ranging over an infinite domain such as the natural numbers or finite strings. Depending on the operations that are allowed on this domain, system executions can then be described as words over an infinite alphabet, possibly equipped with one or several binary relations such as equality or a total order. Those words are usually referred to as data words [BDM+11], [BMSS09]. Many models and results from both areas, parameterized verification and data words, smoothly extend the classical finite-state approach and, in particular, provide decidable instances of the model checking problem. Our concern in this talk will be distributed algorithms, where an unknown number of (identical) processes cooperate to achieve a common goal. However, assuming perfectly identical processes, even simple tasks such as electing a leader cannot always be accomplished. One may, therefore, assume that every process is equipped with a unique process identifier from an unbounded domain, and that identifiers can be compared with one another wrt. a total order. Thus, when modeling distributed algorithms, one has to cope with both sources of infinity mentioned above: the number of processes and infinite data. This may be one reason why there have been only a few approaches to the formal verification of distributed algorithms [KVW12]. In this talk, we survey recent developments in the areas of parameterized verification and data words, and we demonstrate how they can be exploited towards a framework for the formal verification of distributed algorithms [ABG15].