Abstract
In this paper, we illustrate a formal verification method for distributed JavaSpaces applications by analyzing a nontrivial fault tolerant algorithm that solves a typical coordination problem. The problem consists of the computation of an extensive task, performed in parallel by splitting it into smaller and more manageable parts. The proposed solution, based on JavaSpaces coordination primitives, transactions and time-outs, is verified by translating it to the formal language ?CRL, together with the previously developed ?CRL-model of the JavaSpaces architecture, and by using model checking techniques.