Advertisement

Abstract

We provide three methods of verifying concurrent systems which are tolerant of faults in their operating environment — algebraic, logical and transformational. The first is an extension of the bisimulation equivalence, the second is rooted in the Hennessy-Milner logic, and the third involves transformations of CCS processes. Based on the common semantic model of labelled transition systems, which is also used to model faults, all three methods are proved equivalent for certain classes of faults.

Keywords

Binary Relation Transition Relation Operational Semantic Label Transition System Concurrent System 
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. [AH92]
    L. Aceto and M. Hennessy. Termination, deadlock and divergence. Journal of ACM, 39(1):147–187, 1992.Google Scholar
  2. [Cri85]
    F. Cristian. A rigorous approach to fault-tolerant programming. IEEE Transactionsn on Software Engineering, 11(1):23–31, 1985.Google Scholar
  3. [HM85]
    M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137–161, 1985.Google Scholar
  4. [JH87]
    He Jifeng and C.A.R. Hoare. Algebraic specification and proof of a distributed recovery algorithm. Distributed Computing, 2:1–12, 1987.Google Scholar
  5. [Kel76]
    R. Keller. Formal verification of parallel programs. Communications of ACM, 19(7):561–572, 1976.Google Scholar
  6. [Lar87]
    K.G. Larsen. A context dependent equivalence between processes. Theoretical Computer Science, 49:185–215, 1987.Google Scholar
  7. [Liu91]
    Z. Liu. Fault-Tolerant Programming by Transformations. PhD thesis, University of Warwick, 1991.Google Scholar
  8. [LJ91]
    Z. Liu and M. Joseph. Transformations of programs for fault-tolerance. Formal Aspects of Computing, 4:442–469, 1991.Google Scholar
  9. [LT87]
    N. Lynch and M. Tuttle. Hierarchical correctness proofs for distributed algorithms. Technical report, MIT Laboratory for Computer Science, 87.Google Scholar
  10. [LT88]
    K.G. Larsen and B. Thomsen. A modal process logic. In Proc. 3rd Annual Symposium on Logic in Computer Science, pages 203–210, 88.Google Scholar
  11. [Mil80]
    R. Milner. A calculus of communicating systems. LNCS, 92, 1980.Google Scholar
  12. [Mil89]
    R. Milner. Communication and Concurrency. Prentice-Hall International, 1989.Google Scholar
  13. [MP91]
    Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems, volume 1. Springer-Verlag, 1991.Google Scholar
  14. [Nor92]
    J. Nordahl. Specification and Design of Dependable Communicating Systems. PhD thesis, Technical University of Denmark, 1992.Google Scholar
  15. [Par81]
    D. Park. Concurrency and automata on infinite sequences. LNCS, 104, 81.Google Scholar
  16. [Pel91]
    J. Peleska. Design and verification of fault tolerant systems with CSP. Distributed Computing, 5:95–106, 1991.Google Scholar
  17. [PJ93]
    D. Peled and M. Joseph. A compositional approach for fault-tolerance using specification transformation. LNCS, 694, 1993.Google Scholar
  18. [Plo81]
    G. Plotkin. A structural approach to operational semantics. Technical report, Computer Science Department, Aarhus University, 81.Google Scholar
  19. [Pra86]
    V. Pratt. Modeling concurrency with partial orders. International Journal of Parallel Programming, 15(1):33–71, 1986.Google Scholar
  20. [Pra87]
    K.V.S. Prasad. Combinators and Bisimulation Proofs for Restartable Systems. PhD thesis, Department of Computer Science, University of Edinburgh, 1987.Google Scholar
  21. [Sch93]
    H. Schepers. Tracing fault-tolerance. In Proc. 3rd IFIP Working Conference on Dependable Computing for Critical Applications. Springer-Verlag, 1993.Google Scholar
  22. [Wal90]
    D.J. Walker. Bisimulation and divergence. Information and Computation, 85:202–241, 90.Google Scholar
  23. [Win89]
    G. Winskel. An introduction to event structures. LNCS, 354:364–397, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Tomasz Janowski
    • 1
  1. 1.Department of Computer ScienceUniversity of WarwickCoventryUK

Personalised recommendations