Abstract
Many real systems consist of a number of physically distributed components that work independently using their private storage, but also communicate from time to time by explicit message passing. Such systems are called distributed systems. An example is an airline reservation system consisting of a large number of terminals in many different travel agencies and a central data base for keeping the current status of all flights. Here the data base and the terminals are the components of the system, and communication is possible between each terminal and the data base.
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
K.R. Apt, L. Bougé, and Ph. Clermont. Two normal form theorems for CSP programs. Information Processing Letters, 26: 165–171, 1987.
K.R. Apt, N. Francez, and S. Katz. Appraising fairness in distributed languages. Distributed Computing, 2 (4): 226–241, August 1988.
K.R. Apt, N. Francez, and W.P. de Roever. A proof system for communicating sequential processes. ACM Transactions on Programming Languages and Systems, 2 (3): 359–385, 1980.
K.R. Apt. Correctness proofs of distributed termination algorithms. ACM Transactions on Programming Languages and Systems, 8: 388–405, 1986.
L. Bougé and N. Francez. A compositional approach to superimposition. In Proceedings of the 15th Annual ACM Symposium on Principles of Programming Languages, pages 240–249, San Diego, CA, 1988.
R.J.R. Back and R. Kurki-Suonio. Serializability in distributed systems with handshaking. In T. Lepistö and A. Salomaa, editors, Proceedings of International Colloquium on Automata Languages and Programming (ICALP ‘88),pages 52–66, New York, 1988. Lecture Notes in Computer Science 317, Springer-Verlag.
K.M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, New York, 1988.
E.W. Dijkstra, W.H. Feijen, and A.J.M. van Gasteren. Derivation of a termination detection algorithm for distributed computations. Information Processing Letters, 16 (5): 217–219, 1983.
N. Francez, C.A.R. Hoare, D.J. Lehmann, and W.P. de Roever. Semantics of nondeterminism, concurrency and communication. Journal of Computer and System Sciences, 19 (3): 290–308, 1979.
N. Francez, D.J. Lehmann, and A. Pnueli. A linear history semantics for languages for distributed computing. Theoretical Computer Science, 32: 25–46, 1984.
N. Francez and M. Rodeh. Achieving distributed termination without freezing. IEEE Transactions on Software Engineering, SE-8(3): 287–292, 1982.
N. Francez. Distributed termination. ACM Transactions on Programming Languages and Systems, 2 (1): 42–55, 1980.
N. Francez, M. Rodeh, and M. Sintzoff. Distributed termination with interval assertions. In J. Diaz, editor, Proceedings of the International Colloquium on Formalization of Programming Concepts (EATCS), Penniscola, Spain,New York, 1981. Lecture Notes in Computer Science 107, Springer-Verlag.
O. Grumberg, N. Francez, and S. Katz. Fair termination of communicating processes. In Proceedings of the 3rd Annual ACM SIGACT Conference on Principles of Distributed Computing (PODC), pages 254–265, Vancouver, Canada, August 1984.
C.A.R. Hoare. Communicating sequential processes. Communications of the ACM, 21: 666–677, 1978.
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs, NJ, 1985.
J. Hooman and W.P. de Roever. The quest goes on: a survey of proofsystems for partial correctness of CSP. In Current Trends in Concurrency,pages 343–395, New York, 1986. Lecture Notes in Computer Science 224, Springer-Verlag.
S. Katz. A superimposition control construct for distributed systems. Technical Report STP268–87, MCC, Austin, TX, 1987.
G. Levin and D. Gries. A proof technique for communicating sequential processes. Acta Informatica, 15: 281–302, 1981.
F. Mattem. Algorithms for distributed termination detection. Distributed Computing, 2: 161–175, 1987.
E.-R. Olderog. Correctness proof of a CSP program transformation. 1991. In preparation.
G.D. Plotkin. An operational semantics for CSP. In D. Bjorner, editor, Formal Description of Programming Concepts II, pages 199–225, Amsterdam, 1982. North-Holland.
D. Zöbel. Normalform-Transformationen für CSP-Programme. Informatik: Forschung und Entwicklung, 3: 64–76, 1988.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1991 Springer Science+Business Media New York
About this chapter
Cite this chapter
Apt, K.R., Olderog, ER. (1991). Distributed Programs. In: Verification of Sequential and Concurrent Programs. Texts and Monographs in Computer Science. Springer, New York, NY. https://doi.org/10.1007/978-1-4757-4376-0_8
Download citation
DOI: https://doi.org/10.1007/978-1-4757-4376-0_8
Publisher Name: Springer, New York, NY
Print ISBN: 978-1-4757-4378-4
Online ISBN: 978-1-4757-4376-0
eBook Packages: Springer Book Archive