Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Some comments on the assumption-commitment framework for compositional verification of distributed programs

  • Technical Contributions
  • Conference paper
  • First Online:
Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness (REX 1989)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 430))

Abstract

In this paper we investigate the use of assumption-commitment techniques for compositional proofs of safety and liveness properties of networks of processes. An inductive inference strategy to discharge mutually dependent assumptions is investigated. Some existing proof techniques are justified in terms of this framework.

Extended Abstract

Supported by SERC, U.K.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. H. Barringer, R. Kuiper, A. Pnueli, A compositional temporal approach to CSP-like languages, in Proc. IFIP Working Conf., The Role of Abstract Models in Information Processing, Vienna (1985).

    Google Scholar 

  2. N. Francez, A. Pnueli, A proof method for cyclic programs, Acta Informatica 9 (1978).

    Google Scholar 

  3. C.A.R. Hoare, Communicating sequential processes, Comm. ACM 21(8) (1978).

    Google Scholar 

  4. C.A.R. Hoare, A calculus for the total correctness of communicating processes, Sc. Comp. Progr. 1(1,2) (1981).

    Google Scholar 

  5. C.A.R. Hoare, Programs as Predicates, Philosophical. Transactions of the Royal Society, London, Vol. A 312, (1984).

    Google Scholar 

  6. J. Hooman, Compositional specification and verification of distributed real-time systems, to appear in Proceedings of the Workshop on Real-Time Systems — Theory and Applications, York (U.K.), September (1989).

    Google Scholar 

  7. C.B. Jones, Specification and Design of (Parallel) Programs, in Information Processing 83 (R.E.A. Mason, ed.,), North-Holland (1983).

    Google Scholar 

  8. J. Loecks, K. Sieber and R.D. Stansifer, The Foundations of Program Verification, John Wiley and Sons (1984).

    Google Scholar 

  9. J. Misra, K.M. Chandy, Proofs of networks of processes, IEEE Trans. SE 7(4) (1981).

    Google Scholar 

  10. V. Nguyen, D. Gries, S. Owicki, A model and temporal logic proof system for networks of processes, Proc. 12th ACM Symp. on Princ. of Progr. lang. (1985).

    Google Scholar 

  11. S. Owicki, Axiomatic proof techniques for parallel programs, Ph.D. Thesis, Cornell University (1975).

    Google Scholar 

  12. P. Pandya, Compositional Verification of Distributed Programs, Ph.D. Thesis, University of Bombay (1988).

    Google Scholar 

  13. A. Pnueli, “In transition from global to modular temporal reasoning about programs”, in Logics and Models of Concurrent Systems, (K.R. Apt, ed.), Springer-Verlag (1985).

    Google Scholar 

  14. A. Pnueli, Application of temporal logic to the specification and verification of reactive system: a survey of current trends, in Current trends in concurrency, (J.W. de Bakker, W.P. de Roever and G. Rozenberg, eds.), LNCS 224, Springer-Verlag (1986).

    Google Scholar 

  15. W.P. de Roever, ‘The quest for compositionality — a survey of assertion based proof systems for concurrent programs, Part-I, in Proc. of the IFIP conference: The role of abstract models in computer science, (E.J. Neuhold, ed.), North Holland (1985).

    Google Scholar 

  16. E.D. Stark, A Proof Technique for Rely/Guarantee Properties, LNCS 206, (1985).

    Google Scholar 

  17. N. Soundararajan, Correctness proofs of CSP programs, Theoret. Comp. Sci. 24(2) (1983).

    Google Scholar 

  18. N. Soundararajan, Total correctness of CSP programs, Acta Informatica 23 (1986).

    Google Scholar 

  19. Zhou Chaochen, A temporal semantics of CSP, in Proc. of the First Pan Pacific Computer Conference, Melbourne (1985).

    Google Scholar 

  20. J. Zwiers, A. de Bruin, W.P. de Roever, A proof system for partial correctness of dynamic networks of processes, Proc. of the conference on Logics of Programs 1983, LNCS 164 (1984).

    Google Scholar 

  21. J. Zwiers, W.P. de Roever, P. van Emde Boas, Compositionality and concurrent networks: soundness and completeness of a proof system, Proc. 12th ICALP, LNCS 194, Springer-Verlag (1985).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Programming Research Group, Oxford University, 8-11 Keble Road, OX1 3QD, Oxford, UK

    Paritosh K. Pandya

Authors
  1. Paritosh K. Pandya
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

J. W. de Bakker W. -P. de Roever G. Rozenberg

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pandya, P.K. (1990). Some comments on the assumption-commitment framework for compositional verification of distributed programs. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds) Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness. REX 1989. Lecture Notes in Computer Science, vol 430. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52559-9_81

Download citation

  • DOI: https://doi.org/10.1007/3-540-52559-9_81

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-52559-2

  • Online ISBN: 978-3-540-47035-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation