Advertisement

Modelling asynchrony with a synchronous model

  • R. P. Kurshan
  • M. Merritt
  • A. Orda
  • S. R. Sachs
Session 10: Invited Talk
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)

Abstract

The I/O Automaton paradigm of Lynch and Tuttle models asynchrony through an interleaving parallel composition and generalizes more common interleaving models based upon message-passing, such as Hoare's CSP. It is not generally recognized that such interleaving models in fact can be viewed as a special cases of synchronous parallel composition, in which components all move in lock-step. Let A be any set of finite-state I/O Automata drawing actions from a fixed finite set containing a subset Δ, In this article we establish a translation T ∶ A → P to a class of ω-automata P closed under a synchronous parallel composition, for which T is monotonic with respect to implementation relative to Δ, and linear with respect to composition. Thus, for A1,..., A m , B1, ..., B n Σ A and A = A1∥ ⋯ ∥A m , B = B1∥ ⋯ ∥B N , if Δ is the set of actions common to both A and B, then A implements B (in the sense of I/O Automata) if and only if the ω-automaton language containment L(T(A1) ⊗ ⋯ ⊗ T(A m )) ⊂ L(T(B1) ⊗ ⋯ ⊗ T(B n )) obtains, where ∥ denotes the interleaving parallel composition on A and ⊗ denotes the synchronous parallel composition on P. For the class P, we use the L-process model of ω-automata. This result enables one to verify systems specified by I/O Automata through model-checkers such as COSPAN or SMV, that operate on models with synchronous parallel composition. The translation technique generalizes to other interleaving models, although in each case, the translation map must match the specific model. Proofs have been eliminated on account of space limitations. A full version (with all proofs) is available upon request.

Keywords

Boolean Algebra Internal Action Parallel Composition Fairness Constraint Fair Execution 
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

  1. 1.
    Y. Afek, D. S. Greenberg, M. Merritt, and G. Taubenfeld. Computing with Faulty Shared Memory. In Proc. 11th ACM Symp. on Principles of Distributed Computing, 1992.Google Scholar
  2. 2.
    S. Aggarwal, R. P. Kurshan, and K. Sabnani. A Calculus for Protocol Specification and Validation. In Protocol Specification, Testing and Verification III, pages 19–34. North-Holland, 1983.Google Scholar
  3. 3.
    P. Halmos. Lectures on Boolean Algebras. Springer-Verlag, 1974.Google Scholar
  4. 4.
    Z. Har'El and R. P. Kurshan. Modelling concurrent processes. In Proceedings of Internat. Conf. Syst. Sci. Eng., pages 382–385, 1988.Google Scholar
  5. 5.
    C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.Google Scholar
  6. 6.
    R. P. Kurshan. Automata-Theoretic Verification. UC Berkeley Lecture Notes, 1992.Google Scholar
  7. 7.
    R. P. Kurshan. Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, 1994.Google Scholar
  8. 8.
    R. P. Kurshan, M. Merritt, A. Orda, and S. R. Sachs. Formal Verification of a Distributed Algorithm for Accessing Faulty Shared Memory. In Proc. of SBT/IEEE International Telecom. Symp., Rio de Janeiro, Brazil, 1994.Google Scholar
  9. 9.
    N. Lynch and M. Tuttle. Hierarchical Correctness Proofs for Distributed Algorithms. In Proc. 6th ACM Symp. on Principles of Distributed Computing, pages 137–151, 1987.Google Scholar
  10. 10.
    N. Lynch and M. Tuttle. An Introduction to Input/Output Automata. CWI-Quarterly, 2(3):219–246, September 1989.Google Scholar
  11. 11.
    K. L. McMillan. Symbolic Model Checking. Kluwer, 1993.Google Scholar
  12. 12.
    R. Milner. Calculi for Synchrony and Asynchrony. Theoretical Computer Sci., 25:267–340, (1983).Google Scholar
  13. 13.
    E. Sikorski. Boolean Algebras. Springer Verlag, 1969.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • R. P. Kurshan
    • 1
  • M. Merritt
    • 1
  • A. Orda
    • 2
  • S. R. Sachs
    • 3
  1. 1.AT&T Bell LabsMurray HillUSA
  2. 2.Dept. of Elec. Eng.TechnionHaifaIsrael
  3. 3.Dept. of Elec. Eng. and CSU. C. BerkeleyBerkeleyUSA

Personalised recommendations