Skip to main content
SpringerLink
Log in

Verifying mutual exclusion and liveness properties with split preconditions

  • Software Engineering
  • Published:
Journal of Computer Science and Technology Aims and scope Submit manuscript

Abstract

This work is focused on presenting a split precondition approach for the modeling and proving the correctness of distributed algorithms. Formal specification and precise analysis of Peterson's distributed mutual exclusion algorithm for two process has been considered. The proof of properties like, mutual exclusion, liveness, and lockout-freedom have also been presented.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Ammons G, Bodik R, Larus J R. Mining specifications. InProc. 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, January 16–18, 2002, pp.4–16.

  2. Cook J E, Wolf A L. Event-based detection of concurrency. InProc. ACM SIGSOFT'98 Symposium on the Foundation of Software Engineering, Orlando, FL, November 1998, pp.35–45.

  3. Raz O, Koopman P, Shaw M. Semantic anomaly detection in online data sources. InProc. ICSE'02 24th International Conference on Software Engineering, Orlando, Florida, May 22–24, 2002.

  4. Hangal S, Lam M S. Tracking down software bugs using automatic anomaly detection. InProc. ICSE'02 24th International Conference on Software Engineering, Orlando, Florida, May 22–24, 2002.

  5. Win T N, Erust M. Verifying distributed algorithms via dynamic analysis and theorem proving. Technical Report, MIT-LCS-TR-841, MIT Lab for Computer Science, 200 Technology Square, Cambridge, MA, USA, May 2002.

    Google Scholar 

  6. Agha G. Actors: A model of concurrent computation. In Distributed Systems, MIT Press, 1986.

  7. Hoare C A R, Jifeng H E. The prespecification.Information Processing Letters, 1987, 24: 127–132.

    Article  MATH  MathSciNet  Google Scholar 

  8. Hoare C A R. Communicating Sequential Processes. Prentice Hall, 1985.

  9. Chauchen Z, Ravn A P, Hoare C A R. A calculus of durations.Information Processing Letters, 1991, 40(5): 269–276

    Article  MathSciNet  Google Scholar 

  10. Hennessy M, Milner R. Algebraic laws for nondeterminism and concurrency.JACM, 1985, 32(1): 137–161.

    Article  MATH  MathSciNet  Google Scholar 

  11. Holmstrom S. Hennessy-Milner logic with recursion as a specification language, and a refinement calculus based on it. In Specification and Verification of Concurrent Systems, Springer-Verlag, 1990, pp.294–330.

  12. Lamport L. Specifying concurrent program modules.ACM Trans. Programming Languages and Systems, 1982, 5(2): 190–222.

    Article  Google Scholar 

  13. Lamport L. The temporal logic of actions.ACM Trans. Programming Languages and Systems, May 1994, 16(3): 872–923.

    Article  Google Scholar 

  14. Spivey J M. Understanding Z: A Specification Language and Its Formal Semantics. Cambridge University Press, 1988.

  15. Milner R. A calculus of communicating systems.LNCS 92, Springer-Verlag, 1980.

  16. Nelson G. A generalization of Dijkstra's calculus.ACM Trans. Programming Languages and Systems, 1989, 11(4): 517–561.

    Article  Google Scholar 

  17. Apt K R, Francez N, deRover W P. A proof system for communicating sequential processes.ACM Trans. Programming Languages and Systems, 1980, 2(3): 359–385.

    Article  MATH  Google Scholar 

  18. Owicki S, Gries D. Verifying properties of parallel programs: An axiomatic approach.Communications of the ACM, May 1976, 19(5): 279–284.

    Article  MATH  MathSciNet  Google Scholar 

  19. Weber R. Where can I get gas round here?_— An application of a design methodology for distributed systems.LNCS 490, Springer-Verlag, 1991, pp.143–166.

  20. Pau I, Rents I, Schreiner W. Verifying mutual exclusion and liveness properties with TLA. Technical Report OO-05, RISC-Linz, Johannes Kepler University, A-4040 Linz, Austria, January 2000.

    Google Scholar 

  21. Peterson G L. Myths about the mutual exclusion problem.Information Processing Letters, June 1981, 12(3): 115–116.

    Article  MATH  Google Scholar 

  22. Alpern B, Schneider F B. Verifying temporal properties without temporal logic.ACM Trans. Programming Languages, January 1989, 11(1): 147–167.

    Article  MATH  Google Scholar 

  23. Eilenberg S. Automata, Languages and Machines. Vol A, Academic Press, New York, 1974.

    MATH  Google Scholar 

  24. Shankar A U. An introduction to assertional reasoning for concurrent systems.ACM Computing Surveys, September 1993, 25(3): 225–262.

    Article  Google Scholar 

  25. Manna Z, Pnueli A. Temporal Verification of Reactive Ssytems: Safety. Springer-Verlag, New York, 1995.

    Book  Google Scholar 

  26. Manduchi G, Moro M. Automatic verification for a class of distributed systems.Distributed Computing, 2000, 13(3): 127–143.

    Article  Google Scholar 

  27. Finney K. Mathematical notation in formal specification —Too difficult for the masses?IEEE Trans. Software Engineering, February 1996, 22(2): 158–159.

    Article  Google Scholar 

  28. Lynch N A, Tuttle M R. An introduction to input/output automata.CWI-Quarterly, September 1989, 2(3): 219–246.

    MATH  MathSciNet  Google Scholar 

  29. Lynch N A. Distributed Algorithms. Morgan Kaufmann, San Francisco, CA, 1996.

    MATH  Google Scholar 

  30. Garland S J, Lynch N A, Vaziri M. IOA: A language for specifying, programming, and validating distributed systems. Technical Report, MIT Laboratory for Computer Science, 1997.

  31. Garland S J, Guttag J V. A guide to LP: The larch prover. Technical Report 82, Digital Equipment Corporation, Systems Research Center, 31 December 1991

  32. Ernst M D, Cockrell J, Griswold W G, Notkin D. Dynamically discovering likely program invariants to support program evolution.IEEE Trans. Software Engineering, February 2001, 27(2): 1–25.

    Article  Google Scholar 

  33. Chandi K M, Sanders B A. Predicate transformers for reasoning about concurrent computation.Science of Computer programming, 1995, 24: 129–148.

    Article  MathSciNet  Google Scholar 

  34. Singh A K, Bandyopadhyay A K. An algorithm to find the condition for deadlock in a distributed system. InProc. WDC'2000, 2000, pp.70–73.

  35. Dijkstra E W. A Discipline of Programming. Prentice Hall, 1976.

  36. Ben-Ari M. Mathematical Logic for Computer Science. Prentice Hall, 1993.

Download references

Author information

Authors and Affiliations

  1. Department of Computer Engineering, National Institute of Technology, 136119, Kurukshetra, India

    Awadhesh Kumar Singh

  2. Department of Electronics and Telecommunication Engineering, Jadavpur University, 700032, Kolkata, India

    Anup Kumar Bandyopadhyay

Authors
  1. Awadhesh Kumar Singh
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Anup Kumar Bandyopadhyay
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Awadhesh Kumar Singh or Anup Kumar Bandyopadhyay.

Additional information

Regular Paper

Awadhesh Kumar Singh received the B.E. degree in computer science & engineering from Gorakhpur University, Gorakhpur, India in 1988. He received the M.E. and Ph.D. (Engg) degrees in the same area from Jadavpur University, Kolkata, India. He is a faculty member in Computer Engineering Department, National Institute of Technology, Kurukshetra, India. His present research interest is distributed systems.

Anup Kumar Bandyopadhyay received the B.E. (Tel.E.), M.E. (Tel.E.), and Ph.D. (Engg) degrees from Jadavpur University, Calcutta, India in 1968, 1970 and 1983, respectively. From 1970 to 1972 he worked with the Microwave Antenna System Engineering Group of the Indian Space Research Organization. In 1972 he joined the Department of Electronics and Telecommuication Engineering, Jadavpur University, where he is currently a professor. His research interests include computer communication networks and distributed systems.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Singh, A.K., Bandyopadhyay, A.K. Verifying mutual exclusion and liveness properties with split preconditions. J. Comput. Sci. & Technol. 19, 795–802 (2004). https://doi.org/10.1007/BF02973442

Download citation

  • Received:

  • Revised:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF02973442

Keywords

Search

Navigation