Verification of JavaSpaces™ Parallel Programs

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Jaco van de Pol Articles by Miguel Valero Espada

Third International Conference on Application of Concurrency to System Design (ACSD'03)

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," Application of Concurrency to System Design, International Conference on, 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 ={Application of Concurrency to System Design, International Conference on}, 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 - Application of Concurrency to System Design, International Conference on 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 - Application of Concurrency to System Design, International Conference on ER -

Jaco van de Pol, Centrum voor Wiskunde en Informatica

Miguel Valero Espada, Centrum voor Wiskunde en Informatica

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CSD.2003.1207714

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

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.