Verification of JavaSpaces™ parallel programs

Author

Van de Pol, Jaco ; Espada, Miguel Valero

Author_Institution

Centrum voor Wiskunde en Inf., Amsterdam, Netherlands

fYear

2003

Firstpage

196

Lastpage

205

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Application of Concurrency to System Design, 2003. Proceedings. Third International Conference on

Print_ISBN

0-7695-1887-7

Type

conf

DOI

10.1109/CSD.2003.1207714

Filename

1207714