Skip to main content
SpringerLink
Log in

Compositional Systems and Methods

  • Chapter
Verification of Digital and Hybrid Systems

Part of the book series: NATO ASI Series ((NATO ASI F,volume 170))

Abstract

We have already observed that composing finite state processes in parallel leads to an exponential explosion of states in the worst case, which imposes a strong limit on the size and complexity of a system that can be verified by state enumeration methods. Since most Systems by design have a natural division into components or modules, it seems natural to try to reduce the number of processes by taking a divide-and-conquer approach. This means that we separate the specification of system into properties of its components, and verify the properties of the components separately. This of course leaves us the Obligation of proving that the component specifications in turn imply the specification of the entire system. This is called compositional verification.

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. E. M. Clarke, D. E. Long, and K. L. McMillan. Compositional model checking. In Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science, 1989.

    Google Scholar 

  2. E. M. Clarke, D. E. Long, and K. L. McMillan. A language for compositional specification and verification of finite state hardware controllers. In 9th International Symposium on Hardware Description Languages and their Applications, 1989.

    Google Scholar 

  3. W. M. Elseaidy, R. Cleaveland, and J. W . Baugh, Jr. Modeling and verifying active structural control Systems.

    Google Scholar 

  4. O. Grumberg and D. E. Long. Model checking and modular verification. ACM Trans, on Prog. Lang, and Syst., 16(3):843-871, May 1994.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Cadence Berkeley Laboratories, 2001 Addison Street, 3rd floor, 94704-1103, Barkeley, CA, USA

    Kenneth L. McMillan

Authors
  1. Kenneth L. McMillan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Engineering and Natural Sciences , Sabanci University, Orhanli, 81474, Tuzla-Istanbul, Turkey

    M. Kemal Inan

  2. Bell Laboratories, 600 Mountain Avenue, 2A-410 Murray Hill, 07974, NJ, USA

    Robert P. Kurshan

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg New York

About this chapter

Cite this chapter

McMillan, K.L. (2000). Compositional Systems and Methods. In: Inan, M.K., Kurshan, R.P. (eds) Verification of Digital and Hybrid Systems. NATO ASI Series, vol 170. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-59615-5_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-59615-5_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-64052-0

  • Online ISBN: 978-3-642-59615-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation