Abstract
There are now several theories for describing and reasoning about the behavior of communicating systems, where the behavior of a communicating system is described in terms of its capabilities to perform communication actions in cooperation with its environment. In such theories, preorders or equivalences are defined as criteria for when one system is an acceptable substitute or implementation of another. Existing theories of communicating systems define preorders or equivalence relations only between systems with identical sets of communication actions. In many practical design situations, however, it may be desirable to refine a system by changing its set of communication actions. We present a simple method for carrying out such refinements. The method is first formulated in a general setting, and then elaborated in more detail in the trace model and a simple version of the failure model. We illustrate the usefulness of our method by an application to I.451, an ISDN access protocol.
This work was partially supported by the Swedish Board for Technical Development (ESPRIT/BRA project 3096 SPEC)
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
L. Aceto and M. Hennessy. Towards action-refinement in process algebras. Technical Report 3/88, Department of Computer Science, University of Sussex, 1988.
R.J.R. Back. A method for refining atomicity in parallel algorithms. In Proc. PARLE 89, volume 365 of Lecture Notes in Computer Science, pages 199–216, Springer Verlag, 1989.
S.D. Brookes, C.A.R. Hoare, and A.W. Roscoe. A theory of communicating sequential processes. Journal of the ACM, 31(3):560–599, 1984.
S.D. Brookes and A.W. Roscoe. An improved failures model for communicating processes. In Brookes, Roscoe, and Winskel, editors, Proc. Seminar on Concurrency, 1984, volume 197 of Lecture Notes in Computer Science, pages 268–280. Springer Verlag, 1985.
CCITT. CCITT Recomendation I.451:ISDN user-network interface layer 3 specification, 1985.
C.-H. Chow, M. Gouda, and S. Lam. A discipline for constructing multiphase communication protocols. ACM Transactions on Computer Systems, 3(4):315–343, 1985.
R. de Nicola and M. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83–133, 1984.
R. Gorrieri, S. Marchetti, and U. Montanari. A 2CCS: A simple extension of CCS for handling atomic actions. In CAAP '88, volume 299 of Lecture Notes in Computer Science, pages 258–270. Springer Verlag, 1988.
R.J. Glabbeek and W.P. Weijland. Refinement in branching time semantics. Technical Report CS-R8922, CWI, 1989.
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
B. Jonsson. Compositional Verification of Distributed Systems. PhD thesis, Dept. of Computer Systems, Uppsala University, Sweden, Uppsala, Sweden, 1987. Available as report DoCS 87/09.
L. Lamport. On interprocess communication Part I: Basic formalism. Distributed Computing, 1(2):77–85, 1986.
L. Lamport. A theorem on atomicity in distributed algorithms. Distributed Computing, 4(2):59–68, 1990.
N.A. Lynch and M.R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. 6:th ACM Symp. on Principles of Distributed Computing, Vancouver, Canada, pages 137–151, 1987.
E.R. Olderog and C.A.R. Hoare. Specification-oriented semantics for communicating processes. Acta Informatica, 23(1):9–66, 1986.
F.A. Stomp and W.P de Roever. Designing distributed algorithms by means of sequentially phased reasoning. Technical Report 89-8, University of Nijmegen, 1989.
P.H.J. van Eijk, C.A. Vissers, and M. Diaz, editors. The Formal Specification Language LOTOS. North-Holland, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brinksma, E., Jonsson, B., Orava, F. (1991). Refining interfaces of communicating systems. In: Abramsky, S., Maibaum, T.S.E. (eds) TAPSOFT '91. TAPSOFT 1991. Lecture Notes in Computer Science, vol 494. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3540539816_73
Download citation
DOI: https://doi.org/10.1007/3540539816_73
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53981-0
Online ISBN: 978-3-540-46499-0
eBook Packages: Springer Book Archive