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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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)
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)
Corbett, J., Dwyer, M., et al.: Bandera: Extracting Finite-state Models from Java Source Code. In: Proc. ICSE 2000, Limerick, Ireland (2000) (to appear)
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)
Flisakowski, S.: C-Tree distribution, available from http://www.cs.wisc.edu/~flisakow/
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)
Godefroid, P., Hammer, R.S., Jagadeesan, L.: Systematic Software Testing using Verisoft. Bell Labs Technical Journal 3(2) (1998)
Hatcliff, J., Dwyer, M.B., Zheng, H.: Slicing software for model construction. Journal of Higher-Order and Symbolic Computation (2000) to appear
Havelund, K., Pressburger, T.: Model Checking Java Programs Using Java Path- Finder. Int. Journal on Software Tools for Technology Transfer (2000) to appear
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)
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)
Holzmann, G.J.: The model checker Spin. IEEE Trans. on Software Engineering 23(5), 279–295 (1997)
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)
Holzmann, G.J.: An analysis of bitstate hashing. Formal Methods in System De- sign 13(3), 287–305 (1998)
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)
Holzmann, G.J., Smith, M.H.: Automating software feature verification. Bell Labs Technical Journal, Special Issue on Software Complexity (April-June 2000) (to appear)
Kernighan, B.W., Pike, R.: The Practice of Programming, p. 33. Addison-Wesley, Cambridge (1999)
Kernighan, B.W., Ritchie, D.M.: The C Programming Language, 2nd edn. Prentice Hall, Englewood Cliffs (1988)
Millett, L., Teitelbaum, T.: Slicing Promela and its applications to protocol understanding and analysis. In: Proc. 4th Spin Workshop, Paris, France (November 1998)
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)
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)
Tip, F.: A survey of program slicing techniques. Journal of Programming Langu- ages 3(3), 121–189 (1995)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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