Abstract
The decrease of nondeterminism development paradigm that underlies most refinement approaches for concurrent systems is contrasted with the less studied increase of parallelism paradigm used by many protocol designers. We show that the widely used refinement notion of Abadi & Lamport exclusively supports the first paradigm and formulate a generalization that allows derivations of systems applying both paradigms alternatively. We develop the proof technique delayed simulation to prove Abadi & Lamport refinement and its generalization.
Partially supported by the ESPRIT Project 6021 (REACT)
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2), 1991.
A. Arora and M. Gouda. Distributed reset. IEEE Transactions on Computers, 43(9), 1994.
R. J. R. Back. Refinement calculus: Parallel and reactive systems. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, volume 430 of LNCS, 1990.
K. M. Chandy and J. Misra. Parallel Program Design: a Foundation. Addison-Wesley, 1988.
Ching-Tsun Chou and Eli Gafni. Understanding and verifying distributed algorithms using stratified decomposition. In 7th ACM Symp. on Principles of Distributed Computing, 1988.
J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors. Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, volume 430 of LNCS. Springer Verlag, 1990.
R. Gerth. Foundations of compositional program refinement. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, volume 430 of LNCS, 1990.
S. Ghosh and M.H. Karaata. A self stabilizing algorithm for graph coloring. In Proceedings of the 29th Allerton Conference on Control, Communication, and Computing, October 1991.
W. Janssen and J. Zwiers. Protocol design by layered decomposition, a compositional approach. In Proceedings Formal Techniques in Real Time and Fault Tolerant Systems, volume 571 of LNCS, 1992.
B. Jonsson. On decomposing and refining specifications of distributed systems. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, volume 430 of LNCS, 1990.
B. Jonsson. Simulations between specifications of distributed systems. In J. C. M. Baeten and J. F. Groote, editors, CONCUR '91, volume 527 of LNCS, 1991.
B. Jonsson, A. Pnueli, and G. Rump. Proving refinement using transduction. In R. Gerth, editor, Verifying sequentially consistent memory. 1993. To be published as a special issue of Distributed Computing.
S. Katz and D. Peled. Verification of distributed programs using representative interleaving sequences. Distributed Computing, 6, 1992.
S. S. Lam and A. U. Shankar. Refinement and projection of relational specifications. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, volume 430 of LNCS, 1990.
L. Lamport. The temporal logic of actions. Technical Report 79, DEC, Systems Research Center, December 1991. To appear in Transactions on programming Languages and Systems.
N. Lynch and M. Tuttle. Hierachical correctness proofs for distributed algorithms. Proc. of the 6th ACM Symposium on Distributed Computing, 1987.
N. Lynch and F. Vaandrager. Forward and backward simulations for timing based systems. In Real-Time: Theory in Practice, volume 600 of LNCS, 1991.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer Verlag, 1992.
A. Mazurkiewicz. Trace semantics, proceedings of an advanced course. volume 354 of LNCS, Bad Honnef, 1989.
M. Raynal and J.-P. Helary. Synchronization and control of distributed systems and programs. Wiley, 1990.
M. Siegel. Combining development paradigms in stepwise refinement. Technical report, University of Kiel, 1995. To appear.
M. Siegel and F. Stomp. Extending the limits of sequentially phased reasoning. In P. S. Thiagarajan, editor, FST&TCS 14, volume 880 of LNCS, 1994.
E. W. Stark. Proving entailment between conceptual state specifications. Theoretical Computer Science, 56, 1988.
F. Stomp. Preserving specific properties in program development. In Cleaveland, editor, CONCUR '92, volume 630 of LNCS, 1992.
F. Stomp. Structured design of self-stabilizing programs. Proc. of the 2nd Isreal Symposium on Theory of Computing and Systems, 1993.
F. Stomp and W.P. de Roever. A principle for sequentially phased reasoning about distributed algorithms. Formal Aspects of Computing, 6(6), 1994.
Shengzong Zhou, R. Gerth, and R. Kuiper. Transformations preserving properties and properties preserved by transformations in fair transition systems. volume 715 of LNCS, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Siegel, M. (1995). A refinement theory that supports both ’decrease of nondeterminism’ and ’increase of parallelism’. In: Lee, I., Smolka, S.A. (eds) CONCUR '95: Concurrency Theory. CONCUR 1995. Lecture Notes in Computer Science, vol 962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60218-6_28
Download citation
DOI: https://doi.org/10.1007/3-540-60218-6_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60218-7
Online ISBN: 978-3-540-44738-2
eBook Packages: Springer Book Archive