Skip to main content
SpringerLink
Log in
Book cover

International Conference on Foundations of Software Technology and Theoretical Computer Science

FSTTCS 2000: FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science pp 312–324Cite as

A Semantic Theory for Heterogeneous System Design

  • Conference paper
  • First Online:

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

Abstract

This paper extends DeNicola and Hennessy’s testing theory from labeled transition system to Büchi processes and establishes a tight connection between the resulting Büchi must-preorder and satisfaction of linear-time temporal logic (LTL) formulas. An example dealing with the design of a communications protocol testifies to the utility of the theory for heterogeneous system design, in which some components are specified as labeled transition systems and others are given as LTL formulas.

Research support was provided under NASA Contract No. NAS1-97046 and by NSF grant CCR-9988489. The first author was also supported by AFOSR Grant F49620-95-1-0508, ARO Grant P-38682-MA, and NSF Grants CCR-9505562, CCR-9996086, and INT-9996095.

This is a preview of subscription content, 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   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi and L. Lamport. Composing specifications. TOPLAS, 15(1):73–132, 1993. See also: Conjoining Specifications, TOPLAS, 17(3):507-534, 1995.

    Article  Google Scholar 

  2. J. A. Bergstra, A. Ponse, and S.A. Smolka. Handbook of Process Algebra. Elsevier Science, 2000.

    Google Scholar 

  3. E. Brinksma, A. Rensink, and W. Vogler. Fair testing. In CONCUR’ 95, volume 962 of LNCS, pages 313–328. Springer-Verlag, 1995.

    Google Scholar 

  4. S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential processes. J. of the ACM, 31(3):560–599, 1984.

    Article  MATH  MathSciNet  Google Scholar 

  5. E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.

    Google Scholar 

  6. E. M. Clarke, D. E. Long, and K. L. McMillan. Compositional model checking. In LICS’ 89, pages 353–362. IEEE Computer Society Press, 1989.

    Google Scholar 

  7. R. Cleaveland and G. Lüttgen. Model checking is refinement: Relating Büchi testing and linear-time temporal logic. Technical Report 2000–14, Institute for Computer Applications in Science and Engineering, March 2000.

    Google Scholar 

  8. R. DeNicola and M. C. B. Hennessy. Testing equivalences for processes. TCS, 34:83–133, 1983.

    Article  Google Scholar 

  9. R. DeNicola and F. Vaandrager. Three logics for branching bisimulation. J. of the ACM, 42(2):458–487, 1995.

    Article  MATH  Google Scholar 

  10. O. Grumberg and D. E. Long. Model checking and modular verification. TOPLAS, 16(3):843–871, 1994.

    Article  Google Scholar 

  11. M. C. B. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. J. of the ACM, 32(1):137–161, 1985.

    Article  MATH  MathSciNet  Google Scholar 

  12. R. Kaivola and A. Valmari. The weakest compositional semantic equivalence preserving nexttime-less linear temporal logic. In CONCUR’ 92, volume 630 of LNCS, pages 207–221. Springer-Verlag, 1992.

    Chapter  Google Scholar 

  13. O. Kupferman and M. Y. Vardi. Modular model checking. In Compositionality: The Significant Difference, volume 1536 of LNCS. Springer-Verlag, 1997.

    Google Scholar 

  14. R. P. Kurshan. Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, 1994.

    Google Scholar 

  15. L. Lamport. The temporal logic of actions. TOPLAS, 16(3):872–923, 1994.

    Article  Google Scholar 

  16. K. G. Larsen. The expressive power of implicit specifications. TCS, 114(1):119–147, 1993.

    Article  MATH  Google Scholar 

  17. O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Workshop on Logics of Programs, volume 193 of LNCS, pages 196–218. Springer-Verlag, 1985.

    Google Scholar 

  18. M. G. Main. Trace, failure and testing equivalences for communicating processes. J. of Par. Comp., 16(5):383–400, 1987.

    MATH  MathSciNet  Google Scholar 

  19. R. Milner. Communication and Concurrency. Prentice Hall, 1989.

    Google Scholar 

  20. K. Narayan Kumar, R. Cleaveland, and S. A. Smolka. Infinite probabilistic and nonprobabilistic testing. In FSTTCS’ 98, volume 1530 of LNCS, pages 209–220. Springer-Verlag, 1998.

    Google Scholar 

  21. V. Natarajan and R. Cleaveland. Divergence and fair testing. In ICALP’ 95, volume 944 of LNCS, pages 684–695. Springer-Verlag, 1995.

    Google Scholar 

  22. A. Pnueli. The temporal logic of programs. In FOCS’ 77, pages 46–57. IEEE Computer Society Press, 1977.

    Google Scholar 

  23. A. Puhakka and A. Valmari. Weakest-congruence results for livelock-preserving equivalences. In CONCUR’ 99, volume 1664 of LNCS, pages 510–524. Springer-Verlag, 1999.

    Google Scholar 

  24. B. Steffen and A. Ingólfsdóttir. Characteristic formulae for CCS with divergence. Inform. & Comp., 110(1):149–163, 1994.

    Article  MATH  Google Scholar 

  25. C. Stirling. Modal logics for communicating systems. TCS, 49:311–347, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  26. A. Valmari and M. Tiernari. Compositional failure-based semantics models for basic LOTOS. FAC, 7(4):440–468, 1995.

    Article  MATH  Google Scholar 

  27. M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In LICS’ 86, pages 332–344. IEEE Computer Society Press, 1986.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, State University of New York at Stony Brook, 11794-4400, Stony Brook, New York, USA

    Rance Cleaveland

  2. Department of Computer Science, Sheffield University, 211 Portobello Street, S1 4DP, Sheffield, England

    Gerald Lüttgen

Authors
  1. Rance Cleaveland
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gerald Lüttgen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, Indian Institute of Technology, Delhi, Hauz Khas, 110016, New Delhi, India

    Sanjiv Kapoor  & Sanjiva Prasad  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cleaveland, R., Lüttgen, G. (2000). A Semantic Theory for Heterogeneous System Design. In: Kapoor, S., Prasad, S. (eds) FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2000. Lecture Notes in Computer Science, vol 1974. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44450-5_25

Download citation

  • DOI: https://doi.org/10.1007/3-540-44450-5_25

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41413-1

  • Online ISBN: 978-3-540-44450-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation