Title :
Verification of JavaSpaces™ parallel programs
Author :
Van de Pol, Jaco ; Espada, Miguel Valero
Author_Institution :
Centrum voor Wiskunde en Inf., Amsterdam, Netherlands
Abstract :
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 timeouts, 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.
Keywords :
Java; distributed object management; formal languages; formal specification; parallel programming; program verification; software architecture; software fault tolerance; task analysis; μCRL; JavaSpaces; coordination problem solving; distributed termination problem; extensive task computation; fault tolerant algorithm; formal analysis; formal language; formal verification; model checking; parallel computing; software architecture; task splitting; Algorithm design and analysis; Computer architecture; Concurrent computing; Fault tolerance; Formal languages; Formal verification; Java; Mathematical model; Software architecture; State-space methods;
Conference_Titel :
Application of Concurrency to System Design, 2003. Proceedings. Third International Conference on
Print_ISBN :
0-7695-1887-7
DOI :
10.1109/CSD.2003.1207714
