Abstract
Communication between processes in a distributed environment is implemented using either shared memory or message passing paradigm. The message passing paradigm is used more often due to the lesser hardware requirements. MPI is a standardized message passing API with several independent implementations. Specification and verification of distributed systems is generally a challenging task. In this paper we present a case study of specification and verification of MPI based software using abstract state machines (ASMs).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Sunderam, V.S.: PVM: A Framework for Parallel Distributed Computing. In: Concurrency, Practice and Experience, December 1990, vol. 2, pp. 315–339. John Wiley & Sons, Chichester (1990)
MPI-2 Standard, http://www.mpi-forum.org/docs/mpi-20-html/mpi2-report.html
Microsoft Research: AsmL: The Abstract State Machine Language (2002)
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Communications of the ACM archive 21(7), 558–565 (1978)
Campbell, C., Grieskamp, W., Nachmanson, L., et al.: Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer, Technical Report (2005)
Siegel, S.F., Avrunin, G.S.: Modeling wildcard-free MPI programs for verification. In: Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, pp. 95–106 (2005)
Börger, E., Glässer, U.: A formal specification of the PVM architecture. In: IFIP 13th World Computer Congress, vol. 1, pp. 402–409. North-Holland, Amsterdam (2005)
Gurevich, Y.: Evolving Algebras 1993: Lipari Guide. In: Specification and Validation Methods, pp. 9–36. Oxford University Press, Oxford (1993)
Gurevich, Y.: Sequential Abstract State Machines Capture Sequential Algorithms. ACM Transactions on Computational Logic, 77–111 (2000)
Blass, A., Gurevich, Y.: Abstract State Machines Capture Parallel Algorithms. ACM Transactions on Computational Logic, 578–651 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grudenic, I., Bogunovic, N. (2006). Modeling and Verification of MPI Based Distributed Software. In: Mohr, B., Träff, J.L., Worringen, J., Dongarra, J. (eds) Recent Advances in Parallel Virtual Machine and Message Passing Interface. EuroPVM/MPI 2006. Lecture Notes in Computer Science, vol 4192. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11846802_23
Download citation
DOI: https://doi.org/10.1007/11846802_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-39110-4
Online ISBN: 978-3-540-39112-8
eBook Packages: Computer ScienceComputer Science (R0)