Skip to main content
SpringerLink
Log in
Book cover

International SPIN Workshop on Model Checking of Software

SPIN 2000: SPIN Model Checking and Software Verification pp 131–147Cite as

Logic Verification of ANSI-C Code with SPIN

  • Conference paper

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

Abstract

We describe a tool, called AX, that can be used in combination with the model checker Spin to efficiently verify logical properties of distributed software systems implemented in ANSI-standard C [18]. AX, short for Automaton eXtractor, can extract verification models from C code at a user defined level of abstraction. Target applications include telephone switching software, distributed operating systems code, protocol implementations, concurrency control methods, and client-server applications.

This paper discusses how AX is currently implemented, and how we plan to extend it. The tool was used in the formal verification of two substantial software applications: a commercial checkpoint management system and the call processing code for a new telephone switch.

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. Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A note on reliable full- duplex transmission over half-duplex lines. Comm. of the ACM 12(5), 260–261 (1969)

    Article  Google Scholar 

  2. Chan, W., Anderson, R.J., Beame, P., et al.: Model checking large software spe- cifications. IEEE Trans. on Software Engineering 24(7), 498–519 (1998)

    Article  Google Scholar 

  3. Corbett, J., Dwyer, M., et al.: Bandera: Extracting Finite-state Models from Java Source Code. In: Proc. ICSE 2000, Limerick, Ireland (2000) (to appear)

    Google Scholar 

  4. Dwyer, M.B., Pasareanu, C.S.: Filter-based Model Checking of Partial Systems. In: Proc. ACM SIGSOFT Sixth Int. Symp. on the Foundation of Software Enginee- ring (November 1998)

    Google Scholar 

  5. Flisakowski, S.: C-Tree distribution, available from http://www.cs.wisc.edu/~flisakow/

  6. Fossaceca, J.M., Sandoz, J.D., Winterbottom, P.: The PathStarTM access ser- ver: facilitating carrier-scale packet telephony. Bell Labs Technical Journal 3(4), 86–102 (1998)

    Article  Google Scholar 

  7. Godefroid, P., Hammer, R.S., Jagadeesan, L.: Systematic Software Testing using Verisoft. Bell Labs Technical Journal 3(2) (1998)

    Google Scholar 

  8. Hatcliff, J., Dwyer, M.B., Zheng, H.: Slicing software for model construction. Journal of Higher-Order and Symbolic Computation (2000) to appear

    Google Scholar 

  9. Havelund, K., Pressburger, T.: Model Checking Java Programs Using Java Path- Finder. Int. Journal on Software Tools for Technology Transfer (2000) to appear

    Google Scholar 

  10. Holzmann, G.J., Beukers, R.A.: The Pandora protocol development system. In: Proc. 3rd IFIP Symposium on Protocol Specification, Testing, and Verification, PSTV 1983, Zurich, Sw., June 1983, pp. 357–369. North-Holland Publ. Amsterdam (1983)

    Google Scholar 

  11. Holzmann, G.J., Patti, J.: Validating SDL Specifications: An Experiment. In: Proc. Conf on Protocol Specification, Testing, and Verification, June 1989, pp. 317–326. Twente University, Enschede (1989)

    Google Scholar 

  12. Holzmann, G.J.: The model checker Spin. IEEE Trans. on Software Engineering 23(5), 279–295 (1997)

    Article  MathSciNet  Google Scholar 

  13. Holzmann, G.J.: Designing executable abstractions. In: Proc. Formal Methods in Soft- ware Practice, Clearwater Beach, Florida, USA, March 1998. ACM Press, New York (1998)

    Google Scholar 

  14. Holzmann, G.J.: An analysis of bitstate hashing. Formal Methods in System De- sign 13(3), 287–305 (1998)

    MathSciNet  Google Scholar 

  15. Holzmann, G.J., Smith, M.H.: A practical method for the verification of event driven systems. In: Proc. Int. Conf. on Software Engineering, ICSE 1999, Los Angeles, May 1999, pp. 597–608 (1999)

    Google Scholar 

  16. Holzmann, G.J., Smith, M.H.: Automating software feature verification. Bell Labs Technical Journal, Special Issue on Software Complexity (April-June 2000) (to appear)

    Google Scholar 

  17. Kernighan, B.W., Pike, R.: The Practice of Programming, p. 33. Addison-Wesley, Cambridge (1999)

    Google Scholar 

  18. Kernighan, B.W., Ritchie, D.M.: The C Programming Language, 2nd edn. Prentice Hall, Englewood Cliffs (1988)

    Google Scholar 

  19. Millett, L., Teitelbaum, T.: Slicing Promela and its applications to protocol understanding and analysis. In: Proc. 4th Spin Workshop, Paris, France (November 1998)

    Google Scholar 

  20. Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symposium on Fo- undations of Computer Science, Providence, R.I, pp. 46–57 (1977)

    Google Scholar 

  21. Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.E.: Eraser: A dynamic data race detector for multi-threaded programs. ACM Transactions on Computer Systems (TOCS) 15(4), 391–411 (1997)

    Article  Google Scholar 

  22. Tip, F.: A survey of program slicing techniques. Journal of Programming Langu- ages 3(3), 121–189 (1995)

    Google Scholar 

  23. Turing, A.M.: On computable numbers, with an application to the Entscheidungs problem. In: Proc. London Mathematical Soc., Ser. 2{42, pp. 230–265 (1936), (see p. 247)

    Google Scholar 

  24. Visser, W., Park, S., Penix, J.: Applying predicate abstraction to model checking object-oriented programs. In: Proc. 3rd ACM SOGSOFT Workshop on For- mal Methods in Software Practice (August 2000)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Bell Laboratories, Lucent Technologies, Murray Hill, New Jersey, 07974, USA

    Gerard J. Holzmann

Authors
  1. Gerard J. Holzmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Kestrel Technology, Palo Alto, California, USA

    Klaus Havelund

  2.  ,  

    John Penix

  3. SEVEN Networks, 94063, Redwood City, CA, USA

    Willem Visser

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Holzmann, G.J. (2000). Logic Verification of ANSI-C Code with SPIN. In: Havelund, K., Penix, J., Visser, W. (eds) SPIN Model Checking and Software Verification. SPIN 2000. Lecture Notes in Computer Science, vol 1885. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722468_8

Download citation

  • DOI: https://doi.org/10.1007/10722468_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41030-0

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation