Skip to main content
SpringerLink
Log in

Experiences with the Application of Symbolic Model Checking to the Analysis of Software Specifications

  • Conference paper
  • First Online:
Perspectives of System Informatics (PSI 1999)

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

  • 262 Accesses

Abstract

Symbolic model checking is a powerful formal-verification technique which has been used to analyze many hardware systems. In this paper we present our experiences in applying symbolic model checking to software specifications of reactive systems. We have conducted two in depth case studies: one, using the specification of TCAS II (Trafic Alert and Collision Avoidance System II), and the other using a model of an aircraft electrical system. Based on these case studies, we have gained significant experience in how model checking can be used in to analyze software specifications, and have also overcome a number of performance bottlenecks to make the analysis tractable.

The emphasis of this paper is the uses of model checking in the analysis of specifications. We will discuss the types of properties which we were able to evaluate in our case studies. These include specific errors we were able to identify, as well as general properties we were able to establish for the systems. We will also discuss, in more general terms, the potential uses of symbolic model checking in the development process of software specifications.

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. J. M. Atlee and J. Gannon. State-based model checking of event-driven system requirements. IEEE Transactions on Software Engineering, 19(1):24–40, January 1993.

    Article  Google Scholar 

  2. R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(6):677–691, August 1986.

    Article  MATH  Google Scholar 

  3. R. E. Bryant. On the complexity of VLSI implementations and graph representation of boolean functions with applications to integer multiplication. IEEE Transactions on Computers, 40(2):205–213, February 1991.

    Article  Google Scholar 

  4. J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits, 13(4):401–424, April 1994.

    Article  Google Scholar 

  5. W. Chan, R. J. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J. D. Reese. Model checking large software specifications. IEEE Transactions on Software Engineering, 24(7):498–520, July 1998.

    Article  Google Scholar 

  6. W. Chan, R. J. Anderson, P. Beame, D. H. Jones, D. Notkin, and W. E. Warner. Decoupling synchronization from logic for efficient symbolic model checking of statecharts. In Proceedings of the 1999 International Conference on Software Engineering: ICSE 99, Los Angeles, USA, May 1999. To appear.

    Google Scholar 

  7. W. Chan, R. J. Anderson, P. Beame, and D. Notkin. Combining constraint solving and symbolic model checking for a class of systems with non-linear constraints. In O. Grumberg, editor, Computer Aided Verification, 9th International Conference, CAV’97 Proceedings, volume 1254 of Lecture Notes in Computer Science, pages 316–327, Haifa, Israel, June 1997. Springer-Verlag.

    Google Scholar 

  8. W. Chan, R. J. Anderson, P. Beame, and D. Notkin. Improving efficiency of symbolic model checking for state-based system requirements. In M. Young, editor, ISSTA 98: Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 102–112, Clearwater Beach, Florida, USA, March 1998. Published as Software Engineering Notes, 23(2).

    Google Scholar 

  9. E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, April 1986.

    Article  MATH  Google Scholar 

  10. J. Crow and B. L. Di Vito. Formalizing space shuttle software requirements. In Proceedings of the ACM SIGSOFT Workshop on Formal Methods in Software Practice, pages 40–48, January 1996.

    Google Scholar 

  11. D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3):231–274, June 1987.

    Article  MATH  MathSciNet  Google Scholar 

  12. D. Harel and A. Naamad. The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology, 5(4):293–333, October 1996.

    Article  Google Scholar 

  13. D. Harel, A. Pnueli, J. P. Schmidt, and R. Sherman. On the formal semantics of statecharts (extended abstract). In Proceedings: Symposium on Logic in Computer Science, pages 54–64, Ithaca, New York, USA, June 1987. IEEE.

    Google Scholar 

  14. J. Helbig and P. Kelb. An OBDD-representation of statecharts. In Proceedings: The European Design and Test Conference. EDAC, The European Conference on Design Automation. ETC, European Test Conference. EUROASIC, The European Event in ASIC Design, pages 142–149, Paris, France, February/March 1994. IEEE.

    Google Scholar 

  15. M. S. Jaffe, N. G. Leveson, M. P. E. Heimdahl, and B. E. Melhart. Software requirements analysis for real-time process-control systems. IEEE Transactions on Software Engineering, 17(3):241–258, March 1991.

    Article  Google Scholar 

  16. K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

    Google Scholar 

  17. C._R. Nobe and W. E. Warner. Lessons learned from a trial application of requirements modeling using statecharts. In Proceedings of the 2nd International Conference on Requirements Engineering, pages 86–93, Colorado Springs, USA, April 1996. IEEE.

    Google Scholar 

  18. A. Pnueli and M. Shalev. What is in a step: On the semantics of statecharts. In T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software, International Conference TACS’91, volume 526 of Lecture Notes in Computer Science, pages 244–264, Sendai, Japan, September 1991. Springer-Verlag.

    Google Scholar 

  19. J. M. Wing and M. Vaziri-Farahani. A case study in model checking software systems. Science of Computer Programming, 28(2/3):273–299, April 1997.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science and Engineering, University of Washington, Box 352350, Seattle, Washington, 98195-2350, USA

    Richard J. Anderson, Paul Beame, William Chan & David Notkin

Authors
  1. Richard J. Anderson
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Paul Beame
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. William Chan
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. David Notkin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Information Technology, Technical University of Denmark, Bldg. 244, 2800, Lyngby, Denmark

    Dines Bjøner

  2. Computer Science Department, Technical University of Munich, Arcisstr. 21, 80290, Munich, Germany

    Manfred Broy

  3. A.P. Ershov Institute of Informatics Systems, av. Ac. Lavrentyev 6, Novosibirsk, 630090, Russia

    Alexandre V. Zamulin

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Anderson, R.J., Beame, P., Chan, W., Notkin, D. (2000). Experiences with the Application of Symbolic Model Checking to the Analysis of Software Specifications. In: Bjøner, D., Broy, M., Zamulin, A.V. (eds) Perspectives of System Informatics. PSI 1999. Lecture Notes in Computer Science, vol 1755. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46562-6_41

Download citation

  • DOI: https://doi.org/10.1007/3-540-46562-6_41

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-46562-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation