Verification of JavaSpaces TM Parallel Programs
Jaco van de Pol, Miguel Valero Espada · 2003
In this paper, we illustrate a formal verification method for distributed JavaSpaces applications by analyzing a non-trivial fault tolerant algorithm that solves a typical coordi-nation 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 solu-tion, based on JavaSpaces coordination primitives, trans-actions and time-outs, is verified by translating it to the for-mal language μCRL, together with the previously developed μCRL-model of the JavaSpaces architecture, and by using model checking techniques.