This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Third International Conference on Application of Concurrency to System Design (ACSD'03)
Verification of JavaSpaces™ Parallel Programs
Guimar?es, Portugal
June 18-June 20
ISBN: 0-7695-1887-7
ASCII Text
x 
 
Jaco van de Pol, Miguel Valero Espada, "Verification of JavaSpaces™ Parallel Programs," 2010 10th International Conference on Application of Concurrency to System Design, pp. 196, Third International Conference on Application of Concurrency to System Design (ACSD'03), 2003.
 
 
BibTex
x
 
@article{ 10.1109/CSD.2003.1207714,
author = {Jaco van de Pol and Miguel Valero Espada},
title = {Verification of JavaSpaces™ Parallel Programs},
journal ={2010 10th International Conference on Application of Concurrency to System Design},
volume = {0},
year = {2003},
isbn = {0-7695-1887-7},
pages = {196},
doi = {http://doi.ieeecomputersociety.org/10.1109/CSD.2003.1207714},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - 2010 10th International Conference on Application of Concurrency to System Design
TI - Verification of JavaSpaces™ Parallel Programs
SN - 0-7695-1887-7
SP
EP
A1 - Jaco van de Pol,
A1 - Miguel Valero Espada,
PY - 2003
KW - software architecture (JavaSpaces)
KW - Formal analysis and verification
KW - Parallel computing
KW - Distributed termination problem
VL - 0
JA - 2010 10th International Conference on Application of Concurrency to System Design
ER -
 
Jaco van de Pol, Centrum voor Wiskunde en Informatica
Miguel Valero Espada, Centrum voor Wiskunde en Informatica
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.
Index Terms:
software architecture (JavaSpaces), Formal analysis and verification, Parallel computing, Distributed termination problem
Citation:
Jaco van de Pol, Miguel Valero Espada, "Verification of JavaSpaces™ Parallel Programs," acsd, pp.196, Third International Conference on Application of Concurrency to System Design (ACSD'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.