Abstract
Suppose one has a system that has a synchronous interface with its environment. Now, suppose that one refines this system and changes its interface to an asynchronous one. Whatever is meant here by refinement, it cannot be standard (process) refinement since the interface actions have changed; nor is it action refinement in the sense that a process is substituted for an action, as the intention presumably is to allow the system to proceed without having to wait until the environment is willing to synchronize.
In this paper we propose a notion of interface refinement of which changing synchronous to asynchronous communication is an instance; as is in fact the reverse change. This notion of interface refinement is quite powerful; it generalizes all existing methods w.r.t. the class of interface changes that it allows.
The major part of the paper is concerned with developing proof rules with which to verify interface refinement. We use (linear) temporal logic as specification language and an adaptation of the Manna-Pnueli verification framework. The method is illustrated by verifying an interface change in which synchronous communication is replaced by asynchronous send and receive. Proofs of the various theorems and lemma's are delegated to an appendix.
The author is currently working in and partially supported by ESPRIT project P3096: “Formal Methods and Tools for the Development of Distributed and Real-Time Systems (SPEC)”.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253–285, May 1991.
E. Brinksma, B. Jonsson, and F. Orava. Refining interfaces of communicating systems. In S. Abramsky and T. Maibaum, editors, Proceedings of the Colloquium on Combining Paradigms for Software Development, volume 494 of Lecture Notes in Computer Science, pages 297–312. Springer-Verlag, 1991.
K. P. Eswaran, J. N. Gray, R. A. Lorie, and I. L. Traiger. The notions of consistency and predicate locks in a relational database system. Communications of the ACM, 33:151–178, 1976.
R. Gerth. Foundations of compositional program refinement: safety properties. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Proceedings of the NFI/REX Workshop on Stepwise Refinement of Distributed Systems, volume 430 of Lecture Notes in Computer Science, pages 777–809. Springer-Verlag, 1990.
C. A. R. Hoare. Communicating Sequential Processes. International series on computer science. Prentice-Hall, 1986.
C.B. Jones. Systematic Software Development using VDM. Prentice-Hall, second edition, 1990.
B. Jonsson. Simulations between specifications of distributed systems. In J. C. M. Baeten and J. F. Groote, editors, Proceedings of the 2nd International Conference on Concurrency Theory (CONCUR'91), volume 527 of Lecture Notes in Computer Science, pages 346–361. Springer-Verlag, 1991.
L. Lamport. On interprocess communication, Part I: Basic formalism. Distributed Computing, 1(2):77–85, 1986.
L. Lamport. The temporal logic of actions. Technical Report 79, DEC Systems Research Center, Palo Alto, California, December 1991.
N.A. Lynch and M.R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the Fourteenth ACM Symposium on the Principles of Programming Languages, pages 137–151, Munich, Germany, 1987.
N. A. Lynch. Multivalued possibilities mappings. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency, volume 354 of Lecture Notes in Computer Science, pages 519–544. Springer-Verlag, 1989.
R. Milner. Communication and concurrency. International series on computer science. Prentice-Hall, 1989.
Z. Manna and A. Pnueli. The anchored version of the temporal framework. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency, volume 354 of Lecture Notes in Computer Science, pages 201–284. Springer-Verlag, 1989.
Z. Manna and A. Pnueli. Specification and verification of concurrent programs by ∀-automata. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Proc. Temporal Logic in Specification, volume 398 of Lecture Notes in Computer Science, pages 124–165. Springer-Verlag, 1989.
D. Peled, S. Katz, and A. Pnueli. Specifying and proving serializability in temporal logic. IEEE, July 1991.
J. Segers, R. Gerth, and R. Kuiper. Implementing synchronous by asynchronous communication. an example of interface refinement. Technical report, Department of Computing Science, Eindhoven University of Technology, 1992. Deliverable of ESPRIT/BRA project 3096 (SPEC).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gerth, R., Kuiper, R., Segers, J. (1992). Interface refinement in reactive systems. In: Cleaveland, W. (eds) CONCUR '92. CONCUR 1992. Lecture Notes in Computer Science, vol 630. Springer, Berlin, Heidelberg . https://doi.org/10.1007/BFb0084784
Download citation
DOI: https://doi.org/10.1007/BFb0084784
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55822-4
Online ISBN: 978-3-540-47293-3
eBook Packages: Springer Book Archive