Skip to main content
SpringerLink
Log in

Synthesis of Large Concurrent Programs via Pairwise Composition

  • Conference paper
  • First Online:
Book cover CONCUR’99 Concurrency Theory (CONCUR 1999)

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

Included in the following conference series:

Abstract

We present a tractable method for synthesizing arbitrarily large concurrent programs from specifications expressed in temporal logic. Our method does not explicitly construct the global state transition diagram of the program to be synthesized, and thereby avoids state explosion. Instead, it constructs a state transition diagram for each pair of component processes (of the program) that interact. This “pair-program” embodies all possible interactions of the two processes. Our method proceeds in two steps. First, we construct a pair-program for every pair of “connected” processes, and analyze these pair-programs for desired correctness properties. We then take the “pair processes” of the pair-programs, and “compose” them in a certain way to synthesize the large concurrent program. We establish a “large model” theorem which shows that the synthesized large program inherits correctness properties from the pair-programs.

Supported in part by NSF CAREER Grant CCR-9702616 and AFOSR Grant F49620-96-1-0221

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Anuchitanukul and Z. Manna. Realizability and synthesis of reactive modules. In Proc. 6th Intl. CAV Conference, volume 818 of LNCS. Springer-Verlag, 1994.

    Google Scholar 

  2. A. Arora, P. C. Attie, and E. A. Emerson. Synthesis of fault-tolerant concurrent systems. In Proc. 17’th Annual ACM Symposium on Principles of Distributed Computing, pages 173–182, June 1998.

    Google Scholar 

  3. P. C. Attie and E. A. Emerson. Synthesis of concurrent systems for an atomic read/atomic write model of computation (extended abstract). In Proc. 15’th ACM Symposium on Principles of Distributed Computing, pages 111–120, May 1996.

    Google Scholar 

  4. P. C. Attie and E. A. Emerson. Synthesis of concurrent systems with many similar processes. ACM Trans. Program. Lang. Syst.., 20(1):51–115, January 1998.

    Article  Google Scholar 

  5. E. M. Clarke, E. A. Emerson, and P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst.., 8(2):244–263, April 1986.

    Article  MATH  Google Scholar 

  6. P. J. Courtois, H. Heymans, and D. L. Parnas. Concurrent control with readers and writers. Communications of the ACM, 14(10):667–668, 1971.

    Article  Google Scholar 

  7. E. W. Dijkstra. A Discipline of Programming. Prentice-Hall Inc., 1976.

    Google Scholar 

  8. E. W. Dijkstra. Selected Writings on Computing: A Personal Perspective, pages 188–199. Springer-Verlag, New York, 1982.

    MATH  Google Scholar 

  9. D. L. Dill and H. Wong-Toi. Synthesizing processes and schedulers from temporal specifications. In 2’nd Intl.CAV Conference, LNCS vol. 531. Springer-Verlag, 1990.

    Google Scholar 

  10. E. A. Emerson. Temporal and modal logic. In Handbook of Theoretical Computer Science, volume B. The MIT Press/Elsevier, Cambridge, Mass., 1990.

    Google Scholar 

  11. E. A. Emerson and E. M. Clarke. Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program.., 2:241–266, 1982.

    Article  MATH  Google Scholar 

  12. E. A. Emerson and C. Lei. Modalities for model checking: Branching time logic strikes back. Sci. Comput. Program.., 8:275–306, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  13. O. Grumberg and D. E. Long. Model checking and modular verification. ACM Trans. Program. Lang. Syst.., 16(3):843–871, May 1994.

    Article  Google Scholar 

  14. Z. Manna and P. Wolper. Synthesis of communicating processes from temporal logic specifications. ACM Trans. Program. Lang. Syst.., 6(1):68–93, January 1984.

    Article  MATH  Google Scholar 

  15. A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc. 16th ACM Symposium on Principles of Programming Languages, New York, 1989. ACM.

    Google Scholar 

  16. A. Pnueli and R. Rosner. On the synthesis of asynchronous reactive modules. In Proc. 16th ICALP, volume 372 of LNCS, Berlin, 1989. Springer-Verlag.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, Florida International University, Miami, FL, USA

    Paul C. Attie

Authors
  1. Paul C. Attie
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing Science, Eindhoven University of Technology, P.O. Box 513, 5600 MB, Eindhoven, The Netherlands

    Jos C. M. Baeten  & Sjouke Mauw  & 

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Attie, P.C. (1999). Synthesis of Large Concurrent Programs via Pairwise Composition. In: Baeten, J.C.M., Mauw, S. (eds) CONCUR’99 Concurrency Theory. CONCUR 1999. Lecture Notes in Computer Science, vol 1664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48320-9_11

Download citation

  • DOI: https://doi.org/10.1007/3-540-48320-9_11

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66425-3

  • Online ISBN: 978-3-540-48320-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation