Advertisement

A hierarchy of compositional models of I/O-automata (Extended Abstract)

  • Bengt Jonsson
Communications
Part of the Lecture Notes in Computer Science book series (LNCS, volume 452)

Abstract

I/O-automata are communicating systems that are intended to represent distributed systems which communicate with asynchronous message-passing. In contrast to e.g. processes in CCS and CSP, both safety and liveness properties of an I/O-automaton can be adequately represented by its traces (sequences of communication events). In the paper, we investigate a number of compositional trace-based semantical models of I/O-automata. The models differ in their capabilities to represent safety, liveness, termination and divergence properties. We order the models according to how much information they convey about the modeled systems. In addition, we prove that for adjacent pairs of ordered models in the resulting hierarchy, the gap between the two models contains no other compositional model.

Keywords

Semantic Model Compositional Model Proof System Communication Event Finite Sequence 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [BHR84]
    S.D. Brookes, C.A.R. Hoare, and A.W. Roscoe. A theory of communicating sequential processes. J. ACM, 31(3):560–599, 1984.Google Scholar
  2. [BM85]
    R.J.R. Back and H. Mannila. On the suitability of trace semantics for modular proofs of communicating processes. Theoretical Computer Science, 39(1):47–68, 1985.Google Scholar
  3. [Hoa85]
    C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.Google Scholar
  4. [Jon85]
    B. Jonsson. A model and proof system for asynchronous networks. In Proc. 4:th ACM Symp. on Principles of Distributed Computing, pages 49–58, Minaki, Canada, 1985.Google Scholar
  5. [Jon87]
    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.Google Scholar
  6. [Jon90a]
    B. Jonsson. A hiearchy of compositional models of I/O-automata. Technical report, Swedish Institute of Computer Science, 1990.Google Scholar
  7. [Jon90b]
    B. Jonsson. On decomposing and refining specifications of distributed systems. In Proc. REX Workshop on Stepwise Refinement of Distributed Systems, volume 430 of Lecture Notes in Computer Science. Springer Verlag, 1990.Google Scholar
  8. [LT87]
    N.A. Lynch and M.R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. 6th ACM Symp. on Principles of Distributed Computing, pages 137–151, 1987.Google Scholar
  9. [MC81]
    J. Misra and K.M. Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, SE-7(4):417–426, July 1981.Google Scholar
  10. [Mil89]
    R. Milner. Communication and Concurrency. Prentice-Hall, 1989.Google Scholar
  11. [Mis84]
    J. Misra. Reasoning about networks of communicating processes. In INRIA Advanced Nato Study Institute on Logics and Models for Verification and Specification of Concurrent Systems, La Colle sur Loupe, France, 1984.Google Scholar
  12. [MP81]
    Z. Manna and A. Pnueli. The temporal framework for concurrent programs. In Boyer and Moore, editors, The Correctness Problem in Computer Science, pages 215–274. Academic Press, 1981.Google Scholar
  13. [NDGO86]
    V. Nguyen, A. Demers, D. Gries, and S. Owicki. A model and temporal proof system for networks of processes. Distributed Computing, 1(1):7–25, 1986.Google Scholar
  14. [NH84]
    R. de Nicola and M. Hennessy, Testing equivalences for processes. Theoretical Computer Science, 34:83–133, 1984.Google Scholar
  15. [OH86]
    E.R. Olderog and C.A.R. Hoare. Specification-oriented semantics for communicating processes. Acta Informatica, 23(1):9–66, 1986.Google Scholar
  16. [Ora89]
    F. Orava. Verifying safety and deadlock properties of networks of asynchronously communicating processes. In Proc. 9 th IFIP WG6.1 Symp. on Protocol Specification, Testing, and Verification, Twente, Holland, 1989.Google Scholar
  17. [Plo81]
    G. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.Google Scholar
  18. [RR86]
    G.M. Reed and A.W. Roscoe. A timed model for communicating sequential processes. In Proc. ICALP 86, volume 226 of LNCS, pages 314–323. Springer Verlag, 1986.Google Scholar
  19. [RR88]
    G.M. Reed and A.W. Roscoe. Metric spaces as models for real-time concurrency. In Proc. 3 rd Workshop on Math. Found. of Progr. Lang. Semantics, volume 298 of LNCS. Springer Verlag, 1988.Google Scholar
  20. [Sta84]
    E.W. Stark. Foundations of a Theory of Specification for Distributed Systems. PhD thesis, Massachusetts Inst. of Technology, 1984. Available as Report No. MIT/LCS/TR-342.Google Scholar
  21. [vGV87]
    R.J. van Glabbaek and F.W. Vaandrager. Petri net models for algebraic theories of concurency. In Proc. PARLE, volume 259 of LNCS, pages 224–242. Springer Verlag, 1987.Google Scholar
  22. [Zwi89]
    J. Zwiers. Compositionality, Concurrency and Partial Correctness, volume 321 of Lecture Notes in Computer Science. Springer Verlag, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • Bengt Jonsson
    • 1
    • 2
    • 3
  1. 1.Swedish Institute of Computer ScienceStockholm
  2. 2.Dept. of Computer SystemsUppsala UniversitySweden
  3. 3.SICSKistaSweden

Personalised recommendations